ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hm : p.Monic<VAR>hpu : IsUnit p<VAR>a✝ : Nontrivial R<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hm : p.Monic<VAR>hpu : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>h : p * q = 1<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hm : p.Monic<VAR>hpu : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>h : p * q = 1<VAR>this : (p * q).natDegree = p.natDegree + q.natDegree<GOAL>p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hm : p.Monic<VAR>hpu : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>h : p * q = 1<VAR>this : p.natDegree = 0 ∧ q.natDegree = 0<GOAL>p = 1
<VAR>x✝ y✝ x y : ℝ<VAR>hx : x ∈ Icc (-(π / 2)) (π / 2)<VAR>hy : y ∈ Icc (-1) 1<GOAL>x ≤ arcsin y ↔ sin x ≤ y
<VAR>q : ℝ<VAR>hq' : 1 < q<GOAL>eval q (cyclotomic 1 ℝ) ≤ (q + 1) ^ φ 1
<VAR>α : Type u_1<GOAL>ofInt' ↑0 = 0
<VAR>α : Type u_1<GOAL>(Num.ofNat' 0).toZNum = 0
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>ofInt' ↑(pos a) = pos a
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>(Num.pos a).toZNum = pos a
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>ofInt' ↑(neg a) = neg a
<VAR>α : Type u_1<VAR>a : PosNum<GOAL>-(Num.pos a).toZNum = neg a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>c : R<GOAL>derivative ((X + C c) ^ 2) = C 2 * (X + C c)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this : IsCompact s<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝ : IsCompact s<VAR>this : MetricSpace (Subtype s) := inferInstance<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝¹ : IsCompact s<VAR>this✝ : MetricSpace (Subtype s) := inferInstance<VAR>this : CompactSpace (Subtype s)<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝² : IsCompact s<VAR>this✝¹ : MetricSpace (Subtype s) := inferInstance<VAR>this✝ : CompactSpace (Subtype s)<VAR>this : Nonempty (Subtype s)<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝² : IsCompact s<VAR>this✝¹ : MetricSpace (Subtype s) := inferInstance<VAR>this✝ : CompactSpace (Subtype s)<VAR>this : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝² : IsCompact s<VAR>this✝¹ : MetricSpace (Subtype s) := inferInstance<VAR>this✝ : CompactSpace (Subtype s)<VAR>this : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝³ : IsCompact s<VAR>this✝² : MetricSpace (Subtype s) := inferInstance<VAR>this✝¹ : CompactSpace (Subtype s)<VAR>this✝ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<GOAL>ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝³ : IsCompact s<VAR>this✝² : MetricSpace (Subtype s) := inferInstance<VAR>this✝¹ : CompactSpace (Subtype s)<VAR>this✝ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<GOAL>ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<GOAL>ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<GOAL>ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<GOAL>ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<GOAL>ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>AX : ⟦A⟧ = toGHSpace X<GOAL>ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>AX : ⟦A⟧ = toGHSpace X<VAR>BY : ⟦B⟧ = toGHSpace Y<GOAL>ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>AX : ⟦A⟧ = toGHSpace X<VAR>BY : ⟦B⟧ = toGHSpace Y<GOAL>0 ∈ lowerBounds ((fun p => hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y})
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>AX : ⟦A⟧ = toGHSpace X<VAR>BY : ⟦B⟧ = toGHSpace Y<GOAL>hausdorffDist (F '' range Φ') (F '' range Ψ') ∈ (fun p => hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y}
<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>γ : Type w<VAR>inst✝ : MetricSpace γ<VAR>Φ : X → γ<VAR>Ψ : Y → γ<VAR>ha : Isometry Φ<VAR>hb : Isometry Ψ<VAR>xX : X<VAR>h✝ : xX ∈ univ<VAR>s : Set γ := range Φ ∪ range Ψ<VAR>Φ' : X → Subtype s := fun y => ⟨Φ y, ⋯⟩<VAR>Ψ' : Y → Subtype s := fun y => ⟨Ψ y, ⋯⟩<VAR>IΦ' : Isometry Φ'<VAR>IΨ' : Isometry Ψ'<VAR>this✝⁴ : IsCompact s<VAR>this✝³ : MetricSpace (Subtype s) := inferInstance<VAR>this✝² : CompactSpace (Subtype s)<VAR>this✝¹ : Nonempty (Subtype s)<VAR>ΦΦ' : Φ = Subtype.val ∘ Φ'<VAR>ΨΨ' : Ψ = Subtype.val ∘ Ψ'<VAR>this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')<VAR>F : Subtype s → ↥(lp (fun i => ℝ) ⊤) := kuratowskiEmbedding (Subtype s)<VAR>this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')<VAR>A : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>B : NonemptyCompacts ↥(lp (fun n => ℝ) ⊤) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }<VAR>AX : ⟦A⟧ = toGHSpace X<VAR>BY : ⟦B⟧ = toGHSpace Y<GOAL>∃ x ∈ {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y}, hausdorffDist ↑x.1 ↑x.2 = hausdorffDist (F '' range Φ') (F '' range Ψ')
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁶ : Semiring R₁<VAR>inst✝¹⁵ : Semiring R₂<VAR>inst✝¹⁴ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹¹ : TopologicalSpace M'₁<VAR>inst✝¹⁰ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝⁹ : TopologicalSpace M₂<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁷ : TopologicalSpace M₃<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁵ : TopologicalSpace M₄<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : Module R₁ M'₁<VAR>inst✝¹ : Module R₂ M₂<VAR>inst✝ : Module R₃ M₃<VAR>f : M₁ →L[R₁] M₁<GOAL>↑f = LinearMap.id ↔ f = id R₁ M₁
<VAR>s : ℂ<VAR>n : ℕ<GOAL>term δ s n = if n = 1 then 1 else 0
<VAR>s : ℂ<GOAL>term δ s 0 = if 0 = 1 then 1 else 0
<VAR>s : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>term δ s n = if n = 1 then 1 else 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>polar (⇑Q) x (-y) = -polar (⇑Q) x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation α<GOAL>(HOrElse.hOrElse c fun x => empty α) = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation α<GOAL>IsBisimulation fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c s' s : Computation α<VAR>h : (HOrElse.hOrElse s fun x => empty α) = s'<GOAL>BisimO (fun c₁ c₂ => (HOrElse.hOrElse c₂ fun x => empty α) = c₁) (HOrElse.hOrElse s fun x => empty α).destruct s.destruct
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c s' s✝ : Computation α<VAR>h : (HOrElse.hOrElse s✝ fun x => empty α) = s'<VAR>s : Computation α<GOAL>(HOrElse.hOrElse s fun x => (empty α).think) = HOrElse.hOrElse s fun x => empty α
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>(∃ s, a.factors = ↑s) ↔ a ≠ 0
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>a.factors ≠ ⊤ ↔ a ≠ 0
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>x y : ModP K v O hv p<VAR>hx0 : ¬x = 0<VAR>hy0 : ¬y = 0<VAR>hxy0 : ¬x + y = 0<GOAL>preVal K v O hv p (x + y) ≤ max (preVal K v O hv p x) (preVal K v O hv p y)
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>y : ModP K v O hv p<VAR>hy0 : ¬y = 0<VAR>r : O<VAR>hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0<VAR>hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + y = 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + y) ≤ max (preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r)) (preVal K v O hv p y)