ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : Tendsto (fun x => ∑ k ∈ T, f x k) 𝓕 (𝓝 (T.sum g))<GOAL>∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε<GOAL>∀ᶠ (x : α) in 𝓕, dist (∑' (k : β), f x k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε<VAR>n : α<VAR>hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3<VAR>h_suma : Summable fun x => ‖f n x‖<VAR>h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>dist (∑' (k : β), f n k) (∑' (k : β), g k) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε<VAR>n : α<VAR>hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3<VAR>h_suma : Summable fun x => ‖f n x‖<VAR>h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>‖∑ x ∈ T, (f n x - g x) + ∑' (x : ↑(↑T)ᶜ), (f n ↑x - g ↑x)‖ < ε / 3 + (ε / 3 + ε / 3)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε<VAR>n : α<VAR>hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3<VAR>h_suma : Summable fun x => ‖f n x‖<VAR>h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>‖∑ x ∈ T, (f n x - g x)‖ < ε / 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>𝓕 : Filter α<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : α → β → G<VAR>g : β → G<VAR>bound : β → ℝ<VAR>h_sum : Summable bound<VAR>hab : ∀ (k : β), Tendsto (fun x => f x k) 𝓕 (𝓝 (g k))<VAR>h_bound✝ : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k<VAR>h✝¹ : Nonempty β<VAR>h✝ : 𝓕.NeBot<VAR>h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k<VAR>h_sumg : Summable fun x => ‖g x‖<VAR>h_suma✝ : ∀ᶠ (n : α) in 𝓕, Summable fun x => ‖f n x‖<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>S : ℝ<VAR>hS : HasSum bound S<VAR>T : Finset β<VAR>hT : dist (∑ b ∈ T, bound b) S < ε / 3<VAR>h1 : ∑' (k : ↑(↑T)ᶜ), bound ↑k < ε / 3<VAR>h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε<VAR>n : α<VAR>hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3<VAR>h_suma : Summable fun x => ‖f n x‖<VAR>h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k<GOAL>‖∑' (x : ↑(↑T)ᶜ), (f n ↑x - g ↑x)‖ < ε / 3 + ε / 3
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>h : n.minFac ^ n.factorization n.minFac = n<VAR>hn : n ≠ 1<GOAL>IsPrimePow n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k : ℕ<VAR>h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0<VAR>hn : 0 ≠ 1<GOAL>IsPrimePow 0
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>h : n.minFac ^ n.factorization n.minFac = n<VAR>hn : n ≠ 1<VAR>hn' : n ≠ 0<GOAL>IsPrimePow n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>h : n.minFac ^ n.factorization n.minFac = n<VAR>hn : n ≠ 1<VAR>hn' : n ≠ 0<GOAL>0 < n.factorization n.minFac
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i : ι<VAR>hi : i0 ≤ i<GOAL>succ^[(toZ i0 i).toNat] i0 = i
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i✝ i : ι<VAR>hi : i0 ≤ i<GOAL>succ^[Nat.find ⋯] i0 = i
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>hc : Convex ℝ s<VAR>hne : (interior s).Nonempty<VAR>hb : Bornology.IsBounded s<GOAL>∃ h, ⇑h '' interior s = ball 0 1 ∧ ⇑h '' closure s = closedBall 0 1 ∧ ⇑h '' frontier s = sphere 0 1
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this : Nontrivial V<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : (IsFractionRing.fieldEquivOfRingEquiv (frobeniusEquiv p k)) b * a = ↑p ^ m * b<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<GOAL>∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<GOAL>Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>Φ(p, k) ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F) c) = (LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb ≪≫ₗ F) (Φ(p, k) c)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>Φ(p, k) (b • F c) = b • F (Φ(p, k) c)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>Φ(p, k) (b • F₀ c) = b • F₀ (Φ(p, k) c)
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>Φ(p, k) (b • c • x) = b • Φ(p, k) c • x
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>φ(p, k) b • φ(p, k) c • a • x = b • (↑p ^ m * φ(p, k) c) • x
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>(φ(p, k) b * (φ(p, k) c * a)) • x = (b * (↑p ^ m * φ(p, k) c)) • x
<VAR>p : ℕ<VAR>inst✝⁶ : Fact (Nat.Prime p)<VAR>k✝ : Type u_1<VAR>inst✝⁵ : CommRing k✝<VAR>k : Type u_2<VAR>inst✝⁴ : Field k<VAR>inst✝³ : IsAlgClosed k<VAR>inst✝² : CharP k p<VAR>V : Type u_3<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Isocrystal p k V<VAR>h_dim : finrank K(p, k) V = 1<VAR>this✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<VAR>this : Φ(p, k) x ≠ 0<VAR>a : K(p, k)<VAR>ha : a ≠ 0<VAR>hax : Φ(p, k) x = a • x<VAR>b : K(p, k)<VAR>hb : b ≠ 0<VAR>m : ℤ<VAR>hmb : φ(p, k) b * a = ↑p ^ m * b<VAR>F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x<VAR>F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯<VAR>c : StandardOneDimIsocrystal p k m<GOAL>φ(p, k) b * (φ(p, k) c * a) = b * (↑p ^ m * φ(p, k) c)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>hp : Odd p<GOAL>↑p ^ 2 ∣ ∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>hp : Odd p<VAR>h1 : ∀ (i : ℕ), ↑p ^ 2 ∣ (a + ↑p * b) ^ i - (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)<GOAL>↑p ^ 2 ∣ ∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i) - ↑p * a ^ (p - 1)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>hp : Odd p<VAR>h1 : ∀ (i : ℕ), (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) = (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)<GOAL>(Ideal.Quotient.mk (span {↑p ^ 2})) (∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) = (Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>s t : Set α<VAR>z : α<VAR>x y : ↑s<VAR>h : [[s.ordConnectedProj x, s.ordConnectedProj y]] ⊆ s<GOAL>s.ordConnectedProj x = s.ordConnectedProj y
<VAR>V : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>x : V → ℝ<GOAL>(toLin' (lapMatrix ℝ G)) x = 0 ↔ ∀ (i j : V), G.Adj i j → x i = x j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : CommSemiring R₂<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingRight ↔ ∀ (y : M₂), B.flip y = 0 → y = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>j : n<GOAL>↑hA.eigenvectorUnitary *ᵥ Pi.single j 1 = (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>f : α →₀ M<GOAL>(erase a f) a' = if a' = a then 0 else f a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>f : α →₀ M<GOAL>(if a' = a then 0 else f a') = if a' = a then 0 else f a'
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>h : LiftPropAt P g x<VAR>hs : s ∈ 𝓝 x<GOAL>LiftPropWithinAt P g s x
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s t : Set X<VAR>x y : X<VAR>s' : Set X<VAR>r : ENNReal<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>r' : ENNReal<VAR>r0' : r' ≠ 0<VAR>hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y<GOAL>IsMetricSeparated (s ∪ s') t
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s t : Set X<VAR>x y : X<VAR>s' : Set X<VAR>r : ENNReal<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>r' : ENNReal<VAR>r0' : r' ≠ 0<VAR>hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y<GOAL>min r r' ≠ 0
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s t : Set X<VAR>x✝ y✝ : X<VAR>s' : Set X<VAR>r : ENNReal<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>r' : ENNReal<VAR>r0' : r' ≠ 0<VAR>hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y<VAR>x : X<VAR>hx : x ∈ s ∪ s'<VAR>y : X<VAR>hy : y ∈ t<GOAL>x ∈ s → min r r' ≤ edist x y
<VAR>X : Type u_1<VAR>inst✝ : EMetricSpace X<VAR>s t : Set X<VAR>x✝ y✝ : X<VAR>s' : Set X<VAR>r : ENNReal<VAR>r0 : r ≠ 0<VAR>hr : ∀ x ∈ s, ∀ y ∈ t, r ≤ edist x y<VAR>r' : ENNReal<VAR>r0' : r' ≠ 0<VAR>hr' : ∀ x ∈ s', ∀ y ∈ t, r' ≤ edist x y<VAR>x : X<VAR>hx : x ∈ s ∪ s'<VAR>y : X<VAR>hy : y ∈ t<GOAL>x ∈ s' → min r r' ≤ edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : Zero β<VAR>f : α →ₛ β<VAR>x : α<GOAL>x ∈ support ↑f ↔ x ∈ ⋃ y ∈ filter (fun y => y ≠ 0) f.range, ↑f ⁻¹' {y}
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.288867, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>h : HomotopyEquiv C D<GOAL>Homotopy ((F.mapHomologicalComplex c).map h.hom ≫ (F.mapHomologicalComplex c).map h.inv) (𝟙 ((F.mapHomologicalComplex c).obj C))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.288867, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>h : HomotopyEquiv C D<GOAL>Homotopy ((F.mapHomologicalComplex c).map (h.hom ≫ h.inv)) ((F.mapHomologicalComplex c).map (𝟙 C))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.288867, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>h : HomotopyEquiv C D<GOAL>Homotopy ((F.mapHomologicalComplex c).map h.inv ≫ (F.mapHomologicalComplex c).map h.hom) (𝟙 ((F.mapHomologicalComplex c).obj D))
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h✝ k : D ⟶ E<VAR>i : ι<VAR>W : Type u_2<VAR>inst✝² : Category.{?u.288867, u_2} W<VAR>inst✝¹ : Preadditive W<VAR>F : V ⥤ W<VAR>inst✝ : F.Additive<VAR>h : HomotopyEquiv C D<GOAL>Homotopy ((F.mapHomologicalComplex c).map (h.inv ≫ h.hom)) ((F.mapHomologicalComplex c).map (𝟙 D))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<GOAL>∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>↑n ! / ↑n ^ n ≤ 1 / ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>hn : 0 < k.succ<GOAL>↑k.succ ! / ↑k.succ ^ k.succ ≤ 1 / ↑k.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>hn : 0 < k.succ<GOAL>(∏ k_1 ∈ Finset.range k, ↑(k_1 + 1 + 1) * (↑k + 1)⁻¹) * (↑(0 + 1) * (↑k + 1)⁻¹) ≤ (↑k + 1)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>hn : 0 < k.succ<GOAL>(∏ x ∈ Finset.range k, (↑x + 1 + 1) * (↑k + 1)⁻¹) * (↑k + 1)⁻¹ ≤ (↑k + 1)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>hn : 0 < k.succ<VAR>x : ℕ<VAR>hx : x < k<GOAL>0 ≤ (↑x + 1 + 1) * (↑k + 1)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>k : ℕ<VAR>hn : 0 < k.succ<VAR>x : ℕ<VAR>hx : x < k<GOAL>(↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1
<VAR>α : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>inst✝⁴ : UniformSpace α<VAR>inst✝³ : UniformSpace β✝<VAR>inst✝² : UniformSpace γ<VAR>inst✝¹ : UniformSpace δ<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>β : ι' → Type u_6<VAR>inst✝ : (j : ι') → UniformSpace (β j)<VAR>e : ι ≃ ι'<VAR>i : ι<GOAL>UniformContinuous fun x => (Equiv.piCongrLeft β e).toFun x (e i)