ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g✝ : ι → Set X<VAR>g : ι' → ι<VAR>hf : LocallyFinite f<VAR>hg : InjOn g {i | (f (g i)).Nonempty}<VAR>x : X<VAR>t : Set X<VAR>htx : t ∈ 𝓝 x<VAR>htf : {i | (f i ∩ t).Nonempty}.Finite<GOAL>InjOn g (g ⁻¹' {i | (f i ∩ t).Nonempty})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a b : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n<VAR>hb : ¬p ^ 2 ∣ b<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a b : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n<VAR>hb : ¬p ^ 2 ∣ b<VAR>H : p ∣ a ^ n.succ<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a b : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>hpow : p ^ n.succ ∣ a ^ n.succ * b ^ n<VAR>hb : ¬p ^ 2 ∣ b<VAR>hbdiv : p ∣ b ^ n<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>x : α<VAR>hpow : p ^ n.succ ∣ a ^ n.succ * (p * x) ^ n<VAR>hb : ¬p ^ 2 ∣ p * x<VAR>hbdiv : p ∣ (p * x) ^ n<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>x : α<VAR>hb : ¬p ^ 2 ∣ p * x<VAR>hbdiv : p ∣ (p * x) ^ n<VAR>y : α<VAR>hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>x : α<VAR>hb : ¬p ^ 2 ∣ p * x<VAR>hbdiv : p ∣ (p * x) ^ n<VAR>y : α<VAR>hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y<VAR>this : a ^ n.succ * x ^ n = p * y<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>x : α<VAR>hb : ¬p ^ 2 ∣ p * x<VAR>hbdiv : p ∣ (p * x) ^ n<VAR>y : α<VAR>hy : a ^ n.succ * (p * x) ^ n = p ^ n.succ * y<VAR>this : a ^ n.succ * x ^ n = p * y<VAR>hdvdx : p ∣ x ^ n<GOAL>p ^ 2 ∣ p * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>y z : α<VAR>hb : ¬p ^ 2 ∣ p * (p * z)<VAR>hbdiv : p ∣ (p * (p * z)) ^ n<VAR>hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y<VAR>this : a ^ n.succ * (p * z) ^ n = p * y<VAR>hdvdx : p ∣ (p * z) ^ n<GOAL>p ^ 2 ∣ p * (p * z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p a : α<VAR>n : ℕ<VAR>hp : Prime p<VAR>y z : α<VAR>hb : ¬p ^ 2 ∣ p * (p * z)<VAR>hbdiv : p ∣ (p * (p * z)) ^ n<VAR>hy : a ^ n.succ * (p * (p * z)) ^ n = p ^ n.succ * y<VAR>this : a ^ n.succ * (p * z) ^ n = p * y<VAR>hdvdx : p ∣ (p * z) ^ n<GOAL>p * p ∣ p * p * z
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<GOAL>blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<GOAL>blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<VAR>h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)<GOAL>blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<VAR>h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)<VAR>hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0<GOAL>blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<VAR>h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)<VAR>hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0<GOAL>((blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i ∧ 0 < r i) ⊔ blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i ∧ r i ≤ 0) =ᶠ[ae μ] (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i ∧ 0 < r i) ⊔ blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i ∧ r i ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<VAR>h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)<VAR>hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0<GOAL>((blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i ∧ 0 < r i) ∪ blimsup (fun i => cthickening (M * r i) (s i)) atTop fun i => p i ∧ r i ≤ 0) =ᶠ[ae μ] (blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i ∧ 0 < r i) ∪ blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i ∧ r i ≤ 0
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>M : ℝ<VAR>hM : 0 < M<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>this : ∀ (p : ℕ → Prop) {r : ℕ → ℝ}, Tendsto r atTop (𝓝[>] 0) → blimsup (fun i => cthickening (M * r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => cthickening (r i) (s i)) atTop p<VAR>r' : ℕ → ℝ := fun i => if 0 < r i then r i else 1 / (↑i + 1)<VAR>hr' : Tendsto r' atTop (𝓝[>] 0)<VAR>h₀ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (r i) (s i) = cthickening (r' i) (s i)<VAR>h₁ : ∀ (i : ℕ), p i ∧ 0 < r i → cthickening (M * r i) (s i) = cthickening (M * r' i) (s i)<VAR>h₂ : ∀ (i : ℕ), p i ∧ r i ≤ 0 → cthickening (M * r i) (s i) = cthickening (r i) (s i)<VAR>hp : p = fun i => p i ∧ 0 < r i ∨ p i ∧ r i ≤ 0<GOAL>((blimsup (fun x => cthickening (M * r' x) (s x)) atTop fun x => p x ∧ 0 < r x) ∪ blimsup (fun x => cthickening (r x) (s x)) atTop fun x => p x ∧ r x ≤ 0) =ᶠ[ae μ] (blimsup (fun x => cthickening (r' x) (s x)) atTop fun x => p x ∧ 0 < r x) ∪ blimsup (fun i => cthickening (r i) (s i)) atTop fun i => p i ∧ r i ≤ 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : upperCrossingTime a b f N (n + 1) ω ≠ N<GOAL>lowerCrossingTime a b f N n ω < upperCrossingTime a b f N (n + 1) ω
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : upperCrossingTime a b f N (n + 1) ω ≠ N<VAR>h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω<GOAL>stoppedValue f (upperCrossingTime a b f N (n + 1)) ω ≤ a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>a b : ℝ<VAR>f : ℕ → Ω → ℝ<VAR>N n m : ℕ<VAR>ω : Ω<VAR>hab : a < b<VAR>hn : upperCrossingTime a b f N (n + 1) ω ≠ N<VAR>h : lowerCrossingTime a b f N n ω = upperCrossingTime a b f N (n + 1) ω<GOAL>f (lowerCrossingTime a b f N n ω) ω ≤ a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → F<VAR>c : E<VAR>N : Finset α<VAR>h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∑ n ∈ N, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → F<VAR>c : E<VAR>h : ∀ n ∈ ∅, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∑ n ∈ ∅, f n z) c
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : NormedSpace 𝕜 H<VAR>𝕝 : Type u_7<VAR>inst✝³ : NontriviallyNormedField 𝕝<VAR>inst✝² : NormedAlgebra 𝕜 𝕝<VAR>A : Type u_8<VAR>inst✝¹ : NormedRing A<VAR>inst✝ : NormedAlgebra 𝕜 A<VAR>f : α → E → F<VAR>c : E<VAR>a : α<VAR>B : Finset α<VAR>aB : a ∉ B<VAR>hB : (∀ n ∈ B, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun z => ∑ n ∈ B, f n z) c<VAR>h : ∀ n ∈ insert a B, AnalyticAt 𝕜 (f n) c<GOAL>AnalyticAt 𝕜 (fun z => ∑ n ∈ insert a B, f n z) c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>a b : α<GOAL>(a, b) ∈ s ×ˢ s ↔ (a, b) ∈ (range s.card).disjiUnion (fun k => map { toFun := fun i => (i, (f ^ k) i), inj' := ⋯ } s) ⋯
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f : Perm α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>a b : α<GOAL>a ∈ s ∧ b ∈ s ↔ ∃ a_1 < s.card, ∃ a_2 ∈ s, a_2 = a ∧ (⇑f)^[a_1] a_2 = b
<VAR>f✝ : Bool → Bool → Bool<VAR>C : ℕ → Sort u_1<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (bit b n)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>binaryRec z f n = ⋯ ▸ f n.bodd n.div2 (binaryRec z f n.div2)
<VAR>f✝ : Bool → Bool → Bool<VAR>C : ℕ → Sort u_1<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (bit b n)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>binaryRec z f n = cast ⋯ (f n.bodd n.div2 (binaryRec z f n.div2))
<VAR>f✝ : Bool → Bool → Bool<VAR>C : ℕ → Sort u_1<VAR>z : C 0<VAR>f : (b : Bool) → (n : ℕ) → C n → C (bit b n)<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>(if n0 : n = 0 then ⋯.mpr z else ⋯.mpr (f n.bodd n.div2 (binaryRec z f n.div2))) = cast ⋯ (f n.bodd n.div2 (binaryRec z f n.div2))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>hf : Measurable f<VAR>hg : Measurable g<GOAL>∫⁻ (y : β) in s, f y ∂Measure.map g μ = ∫⁻ (x : α) in g ⁻¹' s, f (g x) ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<VAR>hp0 : p ≠ 0<GOAL>(normalize p).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<VAR>hp0 : IsUnit p.leadingCoeff<GOAL>(normalize p).Monic
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Field R<VAR>p q : R[X]<VAR>inst✝ : DecidableEq R<VAR>hp0 : IsUnit p.leadingCoeff<GOAL>IsUnit p.leadingCoeff
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : ↑P α<VAR>a : P.A<VAR>f : P.B a ⟹ α<VAR>xeq : x = ⟨a, f⟩<VAR>pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)<GOAL>LiftP p x
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>x : ↑P α<VAR>a : P.A<VAR>f : P.B a ⟹ α<VAR>xeq : x = ⟨a, f⟩<VAR>pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)<GOAL>(fun i => Subtype.val) <$$> ⟨a, fun i j => ⟨f i j, ⋯⟩⟩ = x
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>f : Vector3 α n.succ → Prop<VAR>x✝ : Exists f<VAR>v : Vector3 α n.succ<VAR>fv : f v<GOAL>f (?m.23397 x✝ v fv :: ?m.23398 x✝ v fv)
<VAR>α : Type u_1<VAR>m n : ℕ<VAR>f : Vector3 α n.succ → Prop<VAR>x✝ : Exists f<VAR>v : Vector3 α n.succ<VAR>fv : f v<GOAL>f v
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : TopologicalSpace ι<VAR>inst✝ : T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<GOAL>IsCompact (closure s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : TopologicalSpace ι<VAR>inst✝ : T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<GOAL>CompactSpace ↑(closure s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : TopologicalSpace ι<VAR>inst✝ : T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<VAR>this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F)<GOAL>CompactSpace ↑(closure s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : TopologicalSpace ι<VAR>inst✝ : T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<VAR>this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F)<VAR>cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<GOAL>CompactSpace ↑(closure s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝¹ : TopologicalSpace ι<VAR>inst✝ : T2Space α<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_clemb : ClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F)<VAR>s : Set ι<VAR>s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q<VAR>this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F)<VAR>cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ Subtype.val) K<VAR>cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ i ∈ closure s, F i x ∈ Q<GOAL>CompactSpace ↑(closure s)
<VAR>G : Type u_1<VAR>inst✝ : DivisionMonoid G<VAR>a b c d : G<VAR>hbd : Commute b d<VAR>hbc : Commute b⁻¹ c<GOAL>a / b * (c / d) = a * c / (b * d)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.reverse.natDegree = f.natDegree - f.natTrailingDegree
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝ : RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>h : x ∈ span R s<GOAL>f x ∈ span R₂ (⇑f '' s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t : Set M<VAR>inst✝ : RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>h : x ∈ span R s<GOAL>f x ∈ map f (span R s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<GOAL>IsTorsionBySet R M {a} ↔ IsTorsionBy R M a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>s : Set R<VAR>a : R<VAR>h : IsTorsionBy R M a<VAR>x : M<GOAL>∀ ⦃a_1 : ↑{a}⦄, ↑a_1 • x = 0
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : (i : ι) → NonAssocSemiring (A i)<VAR>inst✝² : (i : ι) → Module R (A i)<VAR>inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)<VAR>inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)<VAR>x : ⨂[R] (i : ι), A i<GOAL>(mul x) ((tprod R) 1) = x
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>t : Set β<VAR>inst✝ : MeasurableSpace.CountablyGenerated ↑t<VAR>h : NullMeasurable f μ<VAR>hft : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>AEMeasurable f μ
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>h : NullMeasurable f μ<VAR>inst✝ : MeasurableSpace.CountablyGenerated ↑∅<VAR>hft : ∀ᵐ (x : α) ∂μ, f x ∈ ∅<GOAL>AEMeasurable f μ
<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>m0 : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>f✝ g : α → β<VAR>μ ν : Measure α<VAR>f : α → β<VAR>t : Set β<VAR>inst✝ : MeasurableSpace.CountablyGenerated ↑t<VAR>h : NullMeasurable f μ<VAR>hft : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>hne : t.Nonempty<GOAL>AEMeasurable f μ
<VAR>k : ℕ<GOAL>ascFactorial 1 (k + 1) = (k + 1)!
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : Module R M'<VAR>b b₁ : Basis ι R M<VAR>i✝ : ι<VAR>c : R<VAR>x✝ : M<VAR>R₁ : Type u_10<VAR>inst✝⁴ : Semiring R₁<VAR>σ : R →+* R₁<VAR>σ' : R₁ →+* R<VAR>inst✝³ : RingHomInvPair σ σ'<VAR>inst✝² : RingHomInvPair σ' σ<VAR>M₁ : Type u_11<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>f : M → ι → R<VAR>hadd : ∀ (x y : M), f (x + y) = f x + f y<VAR>hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x<VAR>f_eq : ∀ (i : ι), f (b i) = ⇑(Finsupp.single i 1)<VAR>x : M<VAR>i : ι<GOAL>(b.repr x) i = f x i