ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<GOAL>∀ (ε : ℝ≥0), 0 < ε → ↑μ F < ⊤ → limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near : ∀ᶠ (x : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs x) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near : ∀ᶠ (x : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs x) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>limsup (fun i => ↑(μs i) F) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near : ∀ᶠ (x : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs x) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>limsup (fun x => ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2) L ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near : ∀ᶠ (x : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs x) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2 ≤ ↑μ F + ↑ε
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>L : Filter ι<VAR>inst✝³ : MeasurableSpace Ω<VAR>inst✝² : TopologicalSpace Ω<VAR>inst✝¹ : HasOuterApproxClosed Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>μs : ι → FiniteMeasure Ω<VAR>μs_lim : Tendsto μs L (𝓝 μ)<VAR>F : Set Ω<VAR>F_closed : IsClosed F<VAR>hne : L.NeBot<VAR>ε : ℝ≥0<VAR>ε_pos : 0 < ε<VAR>a✝ : ↑μ F < ⊤<VAR>fs : ℕ → Ω →ᵇ ℝ≥0 := F_closed.apprSeq<VAR>key₁ : Tendsto (fun n => ∫⁻ (ω : Ω), ↑((fs n) ω) ∂↑μ) atTop (𝓝 (↑μ F))<VAR>room₁ : ↑μ F < ↑μ F + ↑ε / 2<VAR>M : ℕ<VAR>hM : ∀ b ≥ M, ∫⁻ (ω : Ω), ↑((fs b) ω) ∂↑μ < ↑μ F + ↑ε / 2<VAR>key₂ : Tendsto (fun i => ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs i)) L (𝓝 (∫⁻ (x : Ω), ↑((fs M) x) ∂↑μ))<VAR>room₂ : ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ < ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near : ∀ᶠ (x : ι) in L, ∫⁻ (x : Ω), ↑((fs M) x) ∂↑(μs x) ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<VAR>ev_near' : ∀ᶠ (x : ι) in L, ↑(μs x) F ≤ ∫⁻ (a : Ω), ↑((fs M) a) ∂↑μ + ↑ε / 2<GOAL>↑μ F + ↑ε / 2 + ↑ε / 2 ≤ ↑μ F + ↑ε
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>p₁ p₂ : P<VAR>g : G<GOAL>p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - g
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this : Nonempty ι<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this✝ : Nonempty ι<VAR>this : DecidableEq ι<VAR>x : ι := Classical.arbitrary ι<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this✝ : Nonempty ι<VAR>this : DecidableEq ι<VAR>x : ι := Classical.arbitrary ι<VAR>tx_ne : (t x).Nonempty<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this✝ : Nonempty ι<VAR>this : DecidableEq ι<VAR>x : ι := Classical.arbitrary ι<VAR>y : α<VAR>hy : y ∈ t x<VAR>ι' : Set ι := {x' | x' ≠ x}<VAR>t' : ↑ι' → Finset α := fun x' => (t ↑x').erase y<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this✝ : Nonempty ι<VAR>this : DecidableEq ι<VAR>x : ι := Classical.arbitrary ι<VAR>y : α<VAR>hy : y ∈ t x<VAR>ι' : Set ι := {x' | x' ≠ x}<VAR>t' : ↑ι' → Finset α := fun x' => (t ↑x').erase y<VAR>card_ι' : Fintype.card ↑ι' = n<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t : ι → Finset α<VAR>inst✝ : Fintype ι<VAR>n : ℕ<VAR>hn : Fintype.card ι = n + 1<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>ih : ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α), Fintype.card ι' ≤ n → (∀ (s' : Finset ι'), s'.card ≤ (s'.biUnion t').card) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x<VAR>ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → s.card < (s.biUnion t).card<VAR>this✝ : Nonempty ι<VAR>this : DecidableEq ι<VAR>x : ι := Classical.arbitrary ι<VAR>y : α<VAR>hy : y ∈ t x<VAR>ι' : Set ι := {x' | x' ≠ x}<VAR>t' : ↑ι' → Finset α := fun x' => (t ↑x').erase y<VAR>card_ι' : Fintype.card ↑ι' = n<VAR>f' : ↑ι' → α<VAR>hfinj : Function.Injective f'<VAR>hfr : ∀ (x : ↑ι'), f' x ∈ t' x<GOAL>∃ f, Function.Injective f ∧ ∀ (x : ι), f x ∈ t x
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>w : Word M<VAR>m : M i<GOAL>⟨i, m⟩ ∈ ((equivPair j) w).tail.toList ↔ ⟨i, m⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m⟩
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>w : Word M<VAR>m : M i<GOAL>⟨i, m⟩ ∈ (↑(consRecOn w ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x => if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩ else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔ ⟨i, m⟩ ∈ w.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬w.toList = []), w.toList.head h = ⟨i, m⟩
<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>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<VAR>s : Set M<VAR>x : M<VAR>Φ : PartialDiffeomorph I J M N n<VAR>hx : x ∈ Φ.source<VAR>heq : EqOn f (↑Φ.toPartialEquiv) Φ.source<GOAL>ContMDiffAt I J n f x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s t : Set α<VAR>a✝ a : α<GOAL>{a}⁻¹ = {a⁻¹}
<VAR>x y : ℝ<GOAL>Real.toEReal '' Ioo x y = Ioo ↑x ↑y
<VAR>x y : ℝ<GOAL>WithBot.some '' (WithTop.some '' Ioo x y) = Ioo ↑x ↑y
<VAR>x y : ℝ<GOAL>Ioo ↑↑x ↑↑y = Ioo ↑x ↑y
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a x y x' y' : G₀<VAR>ha : a = 0<GOAL>SemiconjBy a⁻¹ x y ↔ SemiconjBy a y x
<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : IsNoetherianRing ↑Γ(X, U)<GOAL>NoetherianSpace ↑↑(↑U).toPresheafedSpace
<VAR>X : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>inst✝ : IsNoetherianRing ↑Γ(X, U)<VAR>this : IsNoetherianRing ↑Γ(↑U, ⊤)<GOAL>NoetherianSpace ↑↑(↑U).toPresheafedSpace
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>x : A<VAR>n : ℤ<GOAL>(aeval x) (U R n) = eval x (U A n)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>p.IsPrimitive ↔ p.content = 1
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>(∀ (r : R), C r ∣ p → IsUnit r) ↔ IsUnit p.content
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NormalizedGCDMonoid R<VAR>p : R[X]<GOAL>(∀ (r : R), r ∣ p.content → IsUnit r) ↔ IsUnit p.content
<VAR>a✝ b✝ c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>a b n : ℕ<GOAL>a ^ b % n = (a % n) ^ b % n
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hs : IsPreconnected s<VAR>hu : IsOpen u<VAR>h'u : (s ∩ u).Nonempty<VAR>h : closure u ∩ s ⊆ u<VAR>A : s ⊆ u ∪ (closure u)ᶜ<GOAL>s ⊆ u
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hs : IsPreconnected s<VAR>hu : IsOpen u<VAR>h'u : (s ∩ u).Nonempty<VAR>h : closure u ∩ s ⊆ u<VAR>A : s ⊆ u ∪ (closure u)ᶜ<GOAL>Disjoint u (closure u)ᶜ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>N : Submodule R M<VAR>h : N.FG<GOAL>(map N.subtype ⊤).FG
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<VAR>A : (listTransvecRow M).length = r<GOAL>(M * (listTransvecRow M).prod) i (inr ()) = M i (inr ())
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>i : Fin r ⊕ Unit<VAR>A : (listTransvecRow M).length = r<GOAL>(M * (List.take r (listTransvecRow M)).prod) i (inr ()) = M i (inr ())
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>⨅ i, RingHom.ker (WittVector.truncate i) = ⊥
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>∀ x ∈ ⨅ i, RingHom.ker (WittVector.truncate i), x = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>hx : x ∈ ⨅ i, RingHom.ker (WittVector.truncate i)<VAR>n✝ : ℕ<GOAL>x.coeff n✝ = WittVector.coeff 0 n✝
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x : 𝕎 R<VAR>n✝ : ℕ<VAR>hx : ∀ (i i_1 : ℕ), i_1 < i → x.coeff i_1 = 0<GOAL>x.coeff n✝ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<GOAL>s.chainHeight = 0 ↔ s = ∅
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<VAR>X X' : D<VAR>f : (reflector i).obj (A ⨯ B) ⟶ X<VAR>g : X ⟶ X'<GOAL>i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X')).symm ((unitCompPartialBijective B ⋯) (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X')) (prod.lift prod.snd prod.fst ≫ ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X')).symm ((unitCompPartialBijective A ⋯) (((exp.adjunction B).homEquiv A (i.obj X')) (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X')) = i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ ((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv (i.obj ((reflector i).obj B)) (i.obj X)).symm ((unitCompPartialBijective B ⋯) (((exp.adjunction (i.obj ((reflector i).obj A))).homEquiv B (i.obj X)) (prod.lift prod.snd prod.fst ≫ ((exp.adjunction B).homEquiv (i.obj ((reflector i).obj A)) (i.obj X)).symm ((unitCompPartialBijective A ⋯) (((exp.adjunction B).homEquiv A (i.obj X)) (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)) ≫ g
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<VAR>X X' : D<VAR>f : (reflector i).obj (A ⨯ B) ⟶ X<VAR>g : X ⟶ X'<GOAL>i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ uncurry ((unitCompPartialBijective B ⋯) (curry (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective A ⋯) (curry (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X')) = i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ uncurry ((unitCompPartialBijective B ⋯) (curry (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective A ⋯) (curry (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)) ≫ g
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : Reflective i<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : HasFiniteProducts D<VAR>inst✝ : ExponentialIdeal i<VAR>A B : C<VAR>X X' : D<VAR>f : (reflector i).obj (A ⨯ B) ⟶ X<VAR>g : X ⟶ X'<GOAL>i.map (i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ uncurry ((unitCompPartialBijective B ⋯) (curry (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective A ⋯) (curry (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X') (f ≫ g) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X')))) ≫ 𝟙 (i.obj X'))) = i.map (i.fullyFaithfulOfReflective.preimage (prodComparison i ((reflector i).obj A) ((reflector i).obj B) ≫ uncurry ((unitCompPartialBijective B ⋯) (curry (prod.lift prod.snd prod.fst ≫ uncurry ((unitCompPartialBijective A ⋯) (curry (prod.lift prod.snd prod.fst ≫ ((reflectorAdjunction i).homEquiv (A ⨯ B) X) f ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)))) ≫ 𝟙 (i.obj X)) ≫ g)
<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 : s ∈ 𝓝 x<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>α : Type u_1<VAR>a b z : ℤ<GOAL>a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z]