ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this : Nonempty ↑s := Nonempty.to_subtype sne<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this : 0 ≤ ε₂<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝² : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝¹ : 0 ≤ ε₂<VAR>this✝ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝³ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝² : 0 ≤ ε₂<VAR>this✝¹ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝¹<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝⁴ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝³ : 0 ≤ ε₂<VAR>this✝² : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝¹ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝²<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this✝ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<VAR>this : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝⁵ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝⁴ : 0 ≤ ε₂<VAR>this✝³ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝² : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝³<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this✝¹ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<VAR>this✝ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)<VAR>this : hausdorffDist (Fl '' s) (range Fr) ≤ hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝⁶ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝⁵ : 0 ≤ ε₂<VAR>this✝⁴ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝³ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝⁴<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this✝² : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<VAR>this✝¹ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)<VAR>this✝ : hausdorffDist (Fl '' s) (range Fr) ≤ hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)<VAR>this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝⁷ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝⁶ : 0 ≤ ε₂<VAR>this✝⁵ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝⁴ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝⁵<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this✝³ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<VAR>this✝² : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)<VAR>this✝¹ : hausdorffDist (Fl '' s) (range Fr) ≤ hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)<VAR>this✝ : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁<VAR>this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>X : Type u<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>Y : Type v<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>s : Set X<VAR>Φ : ↑s → Y<VAR>ε₁ ε₂ ε₃ : ℝ<VAR>hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁<VAR>hs' : ∀ (x : Y), ∃ y, dist x (Φ y) ≤ ε₃<VAR>H : ∀ (x y : ↑s), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>xs : X<VAR>hxs : xs ∈ s<VAR>Dxs : dist xX xs ≤ ε₁<VAR>sne : s.Nonempty<VAR>this✝⁸ : Nonempty ↑s := Nonempty.to_subtype sne<VAR>this✝⁷ : 0 ≤ ε₂<VAR>this✝⁶ : ∀ (p q : ↑s), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)<VAR>this✝⁵ : MetricSpace (X ⊕ Y) := glueMetricApprox (fun x => ↑x) (fun x => Φ x) (ε₂ / 2 + δ) ⋯ this✝⁶<VAR>Fl : X → X ⊕ Y := inl<VAR>Fr : Y → X ⊕ Y := inr<VAR>Il : Isometry Fl<VAR>Ir : Isometry Fr<VAR>this✝⁴ : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)<VAR>this✝³ : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)<VAR>this✝² : hausdorffDist (Fl '' s) (range Fr) ≤ hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)<VAR>this✝¹ : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁<VAR>this✝ : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ<VAR>this : hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃<GOAL>ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.84737, u_1} C<VAR>inst✝ : Preadditive C<VAR>n m mn : ℤ<VAR>hmn : m + n = mn<VAR>a a' a'' : ℤ<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>K : CochainComplex C ℤ<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>n m mn : ℤ<VAR>hmn : m + n = mn<VAR>a a' a'' : ℤ<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>K : CochainComplex C ℤ<GOAL>(shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K = (shortComplexFunctor C (up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫ (shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫ (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsJacobson R<VAR>P✝ : Ideal R[X]<VAR>hP✝ : P✝.IsMaximal<VAR>P : Ideal R[X]<VAR>hP this : P.IsMaximal<GOAL>(comap C P).IsMaximal
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderClosedTopology α<VAR>f g : β → α<VAR>inst✝ : TopologicalSpace β<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>frontier {b | f b < g b} ⊆ {b | f b = g b}
<VAR>ι✝ : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>l : Filter ι<VAR>p : ι → Prop<VAR>inst✝ : l.IsCountablyGenerated<GOAL>(∀ᶠ (n : ι) in l, p n) ↔ ∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, p (x n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>s t : Set ι<VAR>f g✝ : ι → α<VAR>g : ↑s → ι<VAR>hg : ∀ (i : ↑s), f (g i) ≤ f ↑i<VAR>ht : s.PairwiseDisjoint f<VAR>x y : ↑s<VAR>hxy : g x ≠ g y<GOAL>(Disjoint on f) (g x) (g y)
<VAR>l r : List Char<VAR>c : Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>ValidFor l (List.modifyHead (fun x => c) r) (it.setCurr c)
<VAR>l r : List Char<VAR>c : Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>ValidFor l (List.modifyHead (fun x => c) r) ({ s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }.setCurr c)
<VAR>l r : List Char<VAR>c : Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>ValidFor l (List.modifyHead (fun x => c) r) { s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }
<VAR>l r : List Char<VAR>c : Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<GOAL>{ s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data = l.reverseAux (List.modifyHead (fun x => c) r)
<VAR>l r : List Char<VAR>c : Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<VAR>this : { data := l.reverse ++ r }.set { byteIdx := utf8Len l.reverse } c = { data := l.reverse ++ List.modifyHead (fun x => c) r }<GOAL>{ s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data = l.reverseAux (List.modifyHead (fun x => c) r)
<VAR>l r : List Char<VAR>c : Char<VAR>h : ValidFor l r { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }<VAR>this : { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c = { data := l.reverse ++ List.modifyHead (fun x => c) r }<GOAL>{ s := { data := l.reverse ++ r }.set { byteIdx := utf8Len l } c, i := { byteIdx := utf8Len l } }.s.data = l.reverseAux (List.modifyHead (fun x => c) r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)<VAR>a : α<VAR>b : γ<VAR>hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)<GOAL>di.extend f (i a) = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>i : α → β<VAR>di✝ : DenseInducing i<VAR>inst✝² : TopologicalSpace δ<VAR>f✝ : γ → α<VAR>g : γ → δ<VAR>h : δ → β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : T2Space γ<VAR>f : α → γ<VAR>di : DenseInducing i<VAR>hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)<VAR>a : α<VAR>b : γ<VAR>hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)<GOAL>Tendsto f (𝓝 a) (𝓝 b)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : OrderBot α<VAR>a b c : α<GOAL>Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c
<VAR>z w : ℂ<GOAL>normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
<VAR>z w : ℂ<GOAL>normSq z + normSq (-w) + 2 * (z * (starRingEnd ℂ) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
<VAR>z w : ℂ<GOAL>normSq z + normSq w + -(2 * (z * (starRingEnd ℂ) w).re) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h = CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>RingHom.comp (localizationToStalk R y ≫ (structureSheaf R).presheaf.stalkSpecializes h) (algebraMap R (Localization.AtPrime y.asIdeal)) = RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x) (algebraMap R (Localization.AtPrime y.asIdeal))
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>RingHom.comp ((structureSheaf R).presheaf.stalkSpecializes h) (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) = RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h) ≫ localizationToStalk R x) (algebraMap R (Localization.AtPrime y.asIdeal))
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>RingHom.comp ((structureSheaf R).presheaf.stalkSpecializes h) (RingHom.comp (localizationToStalk R y) (algebraMap R (Localization.AtPrime y.asIdeal))) = RingHom.comp (localizationToStalk R x) (RingHom.comp (CommRingCat.ofHom (PrimeSpectrum.localizationMapOfSpecializes h)) (algebraMap R (Localization.AtPrime y.asIdeal)))
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>RingHom.comp ((structureSheaf R).presheaf.stalkSpecializes h) ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal))) = (IsLocalization.lift ⋯).comp ((IsLocalization.lift ⋯).comp (algebraMap R (Localization.AtPrime y.asIdeal)))
<VAR>R✝ : Type u<VAR>inst✝¹ : CommRing R✝<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>x y : PrimeSpectrum R<VAR>h : x ⤳ y<GOAL>RingHom.comp ((structureSheaf R).presheaf.stalkSpecializes h) (toStalk R y) = toStalk R x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.58695, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsLimit (KernelFork.ofι S.f ⋯)<VAR>inst✝ : S.HasHomology<GOAL>S.Exact
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.58695, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsLimit (KernelFork.ofι S.f ⋯)<VAR>inst✝ : S.HasHomology<GOAL>Epi S.toCycles
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.58695, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : IsLimit (KernelFork.ofι S.f ⋯)<VAR>inst✝ : S.HasHomology<VAR>this : IsSplitEpi S.toCycles<GOAL>Epi S.toCycles
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf✝ : DifferentiableOn ℂ f✝ (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<GOAL>∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ : ℂ → E<VAR>c : ℂ<VAR>r : ℝ<VAR>hf✝ : DifferentiableOn ℂ f✝ (Metric.ball c r)<VAR>z : ℂ<VAR>hz : z ∈ Metric.ball c r<VAR>f : ℂ → ℂ<VAR>hf : DifferentiableOn ℂ f (Metric.ball c r)<VAR>n : ℕ<GOAL>(↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
<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<GOAL>∀ (x : E), ‖0 x‖ ≤ 0 * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>r : ℝ≥0<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(r • μ).toSignedMeasure i = ↑(r • μ.toSignedMeasure) i
<VAR>i j : ℕ<GOAL>(i + j).choose j * i ! * j ! = (i + j)!
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite V<VAR>ι : Sort u_1<VAR>f : ι → G.Finsubgraph<GOAL>↑(⨅ i, f i) = ⨅ i, ↑(f i)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P X Y Z : C<VAR>fst : P ⟶ X<VAR>snd : P ⟶ Y<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>h : IsPullback fst snd f g<VAR>inst✝ : HasPullback f g<GOAL>h.isoPullback.inv ≫ snd = pullback.snd f g
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p q : K[X]<GOAL>RatFunc.mk p q = (algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>z.im ≤ w.im * rexp (dist z w)
<VAR>z✝ w✝ : ℍ<VAR>r R : ℝ<VAR>z w : ℍ<GOAL>log z.im - log w.im ≤ dist z w
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<GOAL>spectralRadius ℂ a = ↑‖a‖₊
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<GOAL>spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)<GOAL>spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)<VAR>h₂ : Tendsto ((fun a => a ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))<GOAL>spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)<VAR>h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))<GOAL>spectralRadius ℂ a ^ 2 = ↑‖a‖₊ ^ 2
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : CompleteSpace A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : CstarRing A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>heq : (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) = (fun x => x ^ 2) ∘ fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)<VAR>h₂ : Tendsto (fun n => ↑‖(a⋆ * a) ^ n‖₊ ^ (1 / ↑n)) atTop (𝓝 (spectralRadius ℂ a ^ 2))<GOAL>↑‖a‖₊ ^ 2 = spectralRadius ℂ (a⋆ * a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>h : μ.InnerRegularCompactLTTop<VAR>f : α → β<VAR>hf : Continuous f<GOAL>(map f μ).InnerRegularWRT IsCompact fun s => MeasurableSet s ∧ (map f μ) s ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>h : μ.InnerRegularCompactLTTop<VAR>f : α → β<VAR>hf : Continuous f<GOAL>∀ (U : Set β), MeasurableSet U ∧ (map f μ) U ≠ ⊤ → MeasurableSet (f ⁻¹' U) ∧ μ (f ⁻¹' U) ≠ ⊤