ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>xmem : x ∈ closedBall b ε<GOAL>y ∈ f '' closedBall b ε
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>xmem : x ∈ closedBall b ε<GOAL>f x = y
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>xmem : x ∈ closedBall b ε<VAR>hx' : Tendsto u atTop (𝓝[closedBall b ε] x)<GOAL>f x = y
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>xmem : x ∈ closedBall b ε<VAR>hx' : Tendsto u atTop (𝓝[closedBall b ε] x)<VAR>T1 : Tendsto (f ∘ u) atTop (𝓝 (f x))<GOAL>f x = y
<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>ε✝ : ℝ<VAR>inst✝ : CompleteSpace E<VAR>f : E → F<VAR>s : Set E<VAR>c : ℝ≥0<VAR>f' : E →L[𝕜] F<VAR>hf : ApproximatesLinearOn f f' s c<VAR>f'symm : f'.NonlinearRightInverse<VAR>ε : ℝ<VAR>b : E<VAR>ε0 : 0 ≤ ε<VAR>hε : closedBall b ε ⊆ s<VAR>y : F<VAR>hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)<VAR>hc : ↑c < (↑f'symm.nnnorm)⁻¹<VAR>If' : 0 < ↑f'symm.nnnorm<VAR>Icf' : ↑c * ↑f'symm.nnnorm < 1<VAR>Jf' : ↑f'symm.nnnorm ≠ 0<VAR>Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0<VAR>g : E → E := fun x => x + f'symm.toFun (y - f x)<VAR>hg : g = fun x => x + f'symm.toFun (y - f x)<VAR>u : ℕ → E := fun n => g^[n] b<VAR>hu : u = fun n => g^[n] b<VAR>usucc : ∀ (n : ℕ), u (n + 1) = g (u n)<VAR>A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y<VAR>B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y<VAR>C : ∀ (n : ℕ) (w : E), dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y → w ∈ closedBall b ε<VAR>D : ∀ (n : ℕ), dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧ dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y<VAR>this : CauchySeq u<VAR>x : E<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>xmem : x ∈ closedBall b ε<VAR>hx' : Tendsto u atTop (𝓝[closedBall b ε] x)<VAR>T1 : Tendsto (f ∘ u) atTop (𝓝 (f x))<VAR>T2 : Tendsto (f ∘ u) atTop (𝓝 y)<GOAL>f x = y
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Icc (n • p) ((n + 1) • p) = univ
<VAR>x✝ y x : ℝ<VAR>hx : x ∈ Icc (-(π / 2)) (π / 2)<GOAL>sin (arcsin (sin x)) = sin x
<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>hp0 : p ≠ 0<GOAL>↑(Multiset.card p.roots) ≤ p.degree
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n m : ℕ<VAR>hmn : m ≤ n<VAR>h : Irreducible (cyclotomic (p ^ n) R)<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n : ℕ<VAR>h : Irreducible (cyclotomic (p ^ n) R)<VAR>hmn : 0 ≤ n<GOAL>Irreducible (cyclotomic (p ^ 0) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>n m : ℕ<VAR>hmn : m ≤ n<VAR>h : Irreducible (cyclotomic (p ^ n) R)<VAR>hm : m > 0<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>m : ℕ<VAR>hm : m > 0<VAR>k : ℕ<VAR>hmn : m ≤ m + k<VAR>h : Irreducible (cyclotomic (p ^ (m + k)) R)<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>m : ℕ<VAR>hm : m > 0<VAR>k : ℕ<VAR>hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)<VAR>hmn : m ≤ m + (k + 1)<VAR>h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>m : ℕ<VAR>hm : m > 0<VAR>k : ℕ<VAR>hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)<VAR>hmn : m ≤ m + (k + 1)<VAR>h : Irreducible (cyclotomic (p ^ (m + (k + 1))) R)<VAR>this : m + k ≠ 0<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>m : ℕ<VAR>hm : m > 0<VAR>k : ℕ<VAR>hk : m ≤ m + k → Irreducible (cyclotomic (p ^ (m + k)) R) → Irreducible (cyclotomic (p ^ m) R)<VAR>hmn : m ≤ m + (k + 1)<VAR>h : Irreducible ((expand R p) (cyclotomic (p ^ (m + k)) R))<VAR>this : m + k ≠ 0<GOAL>Irreducible (cyclotomic (p ^ m) R)
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>F : Type u_3<VAR>inst✝ : PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>h : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : MapsTo g s t<GOAL>eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>F : Type u_3<VAR>inst✝ : PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>h : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : MapsTo g s t<GOAL>∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }), ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ g) (↑i.2 (i_1 + 1))) ((f ∘ g) (↑i.2 i_1)) ≤ ↑C * eVariationOn g s
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>E : Type u_2<VAR>inst✝¹ : PseudoEMetricSpace E<VAR>F : Type u_3<VAR>inst✝ : PseudoEMetricSpace F<VAR>f : E → F<VAR>C : ℝ≥0<VAR>t : Set E<VAR>h : LipschitzOnWith C f t<VAR>g : α → E<VAR>s : Set α<VAR>hg : MapsTo g s t<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<GOAL>∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 (i + 1))) ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 i)) ≤ ↑C * eVariationOn g s
<VAR>A : Type u_1<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasAntidiagonal A<VAR>n : A<VAR>x✝ : A × A<VAR>a b : A<GOAL>(a, b) ∈ map (Equiv.prodComm A A).toEmbedding (antidiagonal n) ↔ (a, b) ∈ antidiagonal n
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts).SupIndep id
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(↑(P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts)).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ c : α<VAR>P✝ : Finpartition a✝<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a✝<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>a : α<VAR>ha : a ∈ ↑(P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts)<VAR>b : α<VAR>hb : b ∈ ↑(P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts)<VAR>h : a ≠ b<GOAL>(Disjoint on id) a b
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ c : α<VAR>P✝ : Finpartition a✝<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a✝<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>a : α<VAR>ha : ∃ a_1 ∈ P.parts.attach, a ∈ (Q ↑a_1 ⋯).parts<VAR>b : α<VAR>hb : ∃ a ∈ P.parts.attach, b ∈ (Q ↑a ⋯).parts<VAR>h : a ≠ b<GOAL>(Disjoint on id) a b
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ c : α<VAR>P✝ : Finpartition a✝<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a✝<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>a b : α<VAR>h : a ≠ b<VAR>A : α<VAR>hA : A ∈ P.parts<VAR>ha : a ∈ (Q ↑⟨A, hA⟩ ⋯).parts<VAR>B : α<VAR>hB : B ∈ P.parts<VAR>hb : b ∈ (Q ↑⟨B, hB⟩ ⋯).parts<GOAL>(Disjoint on id) a b
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ c : α<VAR>P✝ : Finpartition a✝<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a✝<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>a b : α<VAR>h : a ≠ b<VAR>A : α<VAR>hA : A ∈ P.parts<VAR>ha : a ∈ (Q ↑⟨A, hA⟩ ⋯).parts<VAR>hB : A ∈ P.parts<VAR>hb : b ∈ (Q ↑⟨A, hB⟩ ⋯).parts<GOAL>(Disjoint on id) a b
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a✝ b✝ c : α<VAR>P✝ : Finpartition a✝<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a✝<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>a b : α<VAR>h : a ≠ b<VAR>A : α<VAR>hA : A ∈ P.parts<VAR>ha : a ∈ (Q ↑⟨A, hA⟩ ⋯).parts<VAR>B : α<VAR>hB : B ∈ P.parts<VAR>hb : b ∈ (Q ↑⟨B, hB⟩ ⋯).parts<VAR>hAB : A ≠ B<GOAL>(Disjoint on id) a b
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts).sup id = a
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.parts.attach.sup fun x => (Q ↑x ⋯).parts.sup id) = a
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>h : ⊥ ∈ P.parts.attach.biUnion fun i => (Q ↑i ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>h : ∃ a_1 ∈ P.parts.attach, ⊥ ∈ (Q ↑a_1 ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P✝ : Finpartition a<VAR>Q✝ : (i : α) → i ∈ P✝.parts → Finpartition i<VAR>P : Finpartition a<VAR>Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>A : α<VAR>hA : A ∈ P.parts<VAR>h : ⊥ ∈ (Q ↑⟨A, hA⟩ ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ t s : Subgroup α<GOAL>Nat.card α = Nat.card (α ⧸ s) * Nat.card ↥s
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ t s : Subgroup α<GOAL>Nat.card α = Nat.card ((α ⧸ s) × ↥s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>h : affineSpan k (range p) = ⊤<GOAL>0 < Fintype.card ι
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>ι : Type u_4<VAR>inst✝ : Fintype ι<VAR>p : ι → P<VAR>h : affineSpan k (range p) = ⊤<VAR>i : ι<GOAL>0 < Fintype.card ι
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → ℝ<VAR>h_meas : AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hg : 0 ≤ᶠ[ae μ] g<VAR>h_int : Integrable (f + g) μ<GOAL>Integrable f μ
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → ℝ<VAR>h_meas : AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hg : 0 ≤ᶠ[ae μ] g<VAR>h_int : Integrable (f + g) μ<GOAL>∀ᵐ (a : α) ∂μ, ‖f a‖ ≤ (f + g) a
<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>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → ℝ<VAR>h_meas : AEStronglyMeasurable f μ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hg : 0 ≤ᶠ[ae μ] g<VAR>h_int : Integrable (f + g) μ<VAR>a : α<VAR>haf : 0 a ≤ f a<VAR>hag : 0 a ≤ g a<GOAL>‖f a‖ ≤ (f + g) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<GOAL>(insert x s).einfsep = (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<GOAL>(⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) ⊓ s.einfsep ≤ (insert x s).einfsep
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>s t : Set α<GOAL>∀ (x_1 : α), x_1 = x ∨ x_1 ∈ s → ∀ (y : α), y = x ∨ y ∈ s → x_1 ≠ y → ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist x_1 y ∨ s.einfsep ≤ edist x_1 y
<VAR>m n : ℕ<GOAL>↑(m ^ (n + 1)) = ↑m ^ ↑(n + 1)
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hJ : J ∈ π<VAR>J' : Box ι<VAR>hJ' : J' ∈ πi J<GOAL>(π.biUnionTagged πi).tag J' = (πi J).tag J'
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hJ : J ∈ π<VAR>J' : Box ι<VAR>hJ' : J' ∈ πi J<GOAL>(π.biUnionTagged πi).tag J' = (πi (π.biUnionIndex (fun J => (πi J).toPrepartition) J')).tag J'
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<GOAL>Multiset.map (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots = p ^ n • f.roots
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Finite R S<VAR>inst✝ : Module.Free R S<GOAL>(relNorm R) ⊥ = ⊥
<VAR>p x ε : ℝ<VAR>s : Set ℝ<VAR>hs : s ⊆ closedBall x (|p| / 2)<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
<VAR>p x ε : ℝ<VAR>s : Set ℝ<VAR>hs : s ⊆ closedBall x (|p| / 2)<VAR>hε : |p| / 2 ≤ ε<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
<VAR>p x ε : ℝ<VAR>s : Set ℝ<VAR>hs : s ⊆ closedBall x (|p| / 2)<VAR>hε : ε < |p| / 2<GOAL>QuotientAddGroup.mk ⁻¹' closedBall (↑x) ε ∩ s = if ε < |p| / 2 then closedBall x ε ∩ s else s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<GOAL>‖A x‖ ^ 2 = re ⟪((adjoint A).comp A) x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : CompleteSpace E<VAR>inst✝¹ : CompleteSpace G<VAR>inst✝ : CompleteSpace F<VAR>A : E →L[𝕜] F<VAR>x : E<VAR>h : ⟪((adjoint A).comp A) x, x⟫_𝕜 = ⟪A x, A x⟫_𝕜<GOAL>‖A x‖ ^ 2 = re ⟪((adjoint A).comp A) x, x⟫_𝕜
<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>n : Num<GOAL>↑n.bit1 = 2 * ↑n + 1
<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>n : Num<GOAL>2 * ↑n + ↑1 = 2 * ↑n + 1
<VAR>n m : ℕ<VAR>h : optParam (¬last (n + 1) = 0) ⋯<GOAL>(last (n + 1)).pred h = last n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>s : Set E<VAR>x : E<GOAL>x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)