ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<VAR>hmncp : m.gcd n = 1<VAR>hm2 : m % 2 = 1<VAR>hn2 : n % 2 = 0<GOAL>h.IsPrimitiveClassified
<VAR>x y z : ℤ<VAR>h : PythagoreanTriple x y z<VAR>hc : x.gcd y = 1<VAR>hyo : y % 2 = 1<VAR>hzpos : 0 < z<VAR>h0 : ¬x = 0<VAR>v : ℚ := ↑x / ↑z<VAR>w : ℚ := ↑y / ↑z<VAR>hq : v ^ 2 + w ^ 2 = 1<VAR>hvz : v ≠ 0<VAR>hw1 : w ≠ -1<VAR>hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0<VAR>hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}<VAR>q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩<VAR>ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)<VAR>m : ℤ := ↑q.den<VAR>n : ℤ := q.num<VAR>hm0 : m ≠ 0<VAR>hq2 : q = ↑n / ↑m<VAR>hm2n2 : 0 < m ^ 2 + n ^ 2<VAR>hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0<VAR>hx1 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → (1 - (j / k) ^ 2) / (1 + (j / k) ^ 2) = (k ^ 2 - j ^ 2) / (k ^ 2 + j ^ 2)<VAR>hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)<VAR>hx2 : ∀ {j k : ℚ}, k ≠ 0 → k ^ 2 + j ^ 2 ≠ 0 → 2 * (j / k) / (1 + (j / k) ^ 2) = 2 * k * j / (k ^ 2 + j ^ 2)<VAR>hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)<VAR>hnmcp : n.gcd m = 1<VAR>hmncp : m.gcd n = 1<VAR>hm2 : m % 2 = 1<VAR>hn2 : n % 2 = 1<GOAL>h.IsPrimitiveClassified
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : Fintype.card (E ≃ₐ[F] E) = finrank F E<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : Fintype.card (E ≃ₐ[F] E) = finrank F E<GOAL>IntermediateField.fixedField ⊤ = ⊥
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : Fintype.card (E ≃ₐ[F] E) = finrank F E<VAR>p : 0 < finrank (↥(IntermediateField.fixedField ⊤)) E<GOAL>IntermediateField.fixedField ⊤ = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<GOAL>∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hμT : μ T ≠ 0<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hμT : μ T ≠ 0<VAR>hTm : NullMeasurableSet T μ<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hμT : μ T ≠ 0<VAR>hTm : NullMeasurableSet T μ<VAR>x : α<VAR>hxt : x ∈ T<VAR>m : ℕ<VAR>hm₀ : m ≠ 0<VAR>hmt : f^[m] x ∈ T<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hμT : μ T ≠ 0<VAR>hTm : NullMeasurableSet T μ<VAR>x : α<VAR>hxt : x ∈ T<VAR>m : ℕ<VAR>hm₀ : m ≠ 0<VAR>hmt : f^[m] x ∈ T<GOAL>N + m > N
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Conservative f μ<VAR>hs : NullMeasurableSet s μ<VAR>h0 : μ s ≠ 0<VAR>t : ℕ → Set α := fun n => s ∩ f^[n] ⁻¹' s<VAR>H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0<VAR>N : ℕ<VAR>hN : μ (t N) ≠ 0<VAR>hmax : ∀ n > N, μ (t n) = 0<VAR>htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ<VAR>T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n<VAR>hμT : μ T ≠ 0<VAR>hTm : NullMeasurableSet T μ<VAR>x : α<VAR>hxt : x ∈ T<VAR>m : ℕ<VAR>hm₀ : m ≠ 0<VAR>hmt : f^[m] x ∈ T<GOAL>x ∈ f^[N + m] ⁻¹' s
<VAR>a : ℤ<GOAL>J(a | 0) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>s t : Set α<VAR>x : α<VAR>ht : ContinuousWithinAt f t x<VAR>h : ContinuousWithinAt f (s \ t) x<GOAL>s ⊆ s \ t ∪ t
<VAR>x : ℝ<VAR>hx : |x| ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hxc : Complex.abs ↑x ≤ 1<GOAL>|rexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial| ≤ |x| ^ n * (↑n.succ / (↑n.factorial * ↑n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g✝ : γ → α<VAR>κ : Kernel α (β × γ)<VAR>a : α<VAR>g : γ × β → ℝ≥0∞<VAR>hg : Measurable g<GOAL>∫⁻ (c : γ × β), g c ∂κ.swapRight a = ∫⁻ (bc : β × γ), g bc.swap ∂κ a
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Balanced<VAR>hr : r.Balanced<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'<GOAL>All P (l.balanceL x r) ↔ All P l ∧ P x ∧ All P r
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a < 1 / b ↔ b < 1 / a
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<VAR>H : (⇑S.subtype ⁻¹' (((fun p => p.1 * p.2) ∘ fun p => (p.1⁻¹, p.2)) '' K ×ˢ L)ᶜ)ᶜ.Finite<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<VAR>H : (Subtype.val ⁻¹' ((fun a => a.1⁻¹ * a.2) '' K ×ˢ L)).Finite<GOAL>{γ | (fun x => γ • x) '' K ∩ L ≠ ∅}.Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<VAR>H : (Subtype.val ⁻¹' ((fun a => a.1⁻¹ * a.2) '' K ×ˢ L)).Finite<GOAL>(⇑S.equivOp ⁻¹' {γ | (fun x => γ • x) '' K ∩ L ≠ ∅}).Finite
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<VAR>H : (Subtype.val ⁻¹' ((fun a => a.1⁻¹ * a.2) '' K ×ˢ L)).Finite<VAR>x : ↥S<GOAL>x ∈ ⇑S.equivOp ⁻¹' {γ | (fun x => γ • x) '' K ∩ L ≠ ∅} ↔ x ∈ Subtype.val ⁻¹' ((fun a => a.1⁻¹ * a.2) '' K ×ˢ L)
<VAR>G : Type w<VAR>H✝ : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : Group G<VAR>inst✝² : TopologicalGroup G<VAR>S✝ : Subgroup G<VAR>inst✝¹ : S✝.Normal<VAR>inst✝ : IsClosed ↑S✝<VAR>S : Subgroup G<VAR>hS : Tendsto (⇑S.subtype) cofinite (cocompact G)<VAR>K L : Set G<VAR>hK : IsCompact K<VAR>hL : IsCompact L<VAR>this : Continuous fun p => (p.1⁻¹, p.2)<VAR>H : (Subtype.val ⁻¹' ((fun a => a.1⁻¹ * a.2) '' K ×ˢ L)).Finite<VAR>x : ↥S<GOAL>S.equivOp x • K ∩ L ≠ ∅ ↔ ∃ a b, (a, b) ∈ K ×ˢ L ∧ a⁻¹ * b = ↑x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p q : Seminorm 𝕝 E<VAR>hq : Continuous ⇑q<VAR>hpq : p ≤ q<GOAL>Continuous ⇑p
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p q : Seminorm 𝕝 E<VAR>hq : Continuous ⇑q<VAR>hpq : p ≤ q<VAR>r : ℝ<VAR>hr : r > 0<GOAL>IsOpen (q.ball 0 r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedRing 𝕝<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : Module 𝕝 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p q : Seminorm 𝕝 E<VAR>hq : Continuous ⇑q<VAR>hpq : p ≤ q<VAR>r : ℝ<VAR>hr : r > 0<GOAL>IsOpen {y | q y < r}
<VAR>a b c : Ordinal.{u_1}<VAR>hb : b < a<VAR>hc : c < a<VAR>H : a ≤ b + c<GOAL>∃ b c, b < a ∧ c < a ∧ b + c = a
<VAR>a b c : Ordinal.{u_1}<VAR>hb : b < a<VAR>hc : c < a<VAR>H : a ≤ b + c<VAR>hab : a - b = a<GOAL>False
<VAR>a b c : Ordinal.{u_1}<VAR>hb : b < a<VAR>hc : c < a<VAR>H : a ≤ c<VAR>hab : a - b = a<GOAL>False
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<VAR>w : Set τ := (⋂ u ∈ g, u) ∩ v<VAR>hw₂ : w ∈ f<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<VAR>w : Set τ := (⋂ u ∈ g, u) ∩ v<VAR>hw₂ : w ∈ f<VAR>hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<VAR>w : Set τ := (⋂ u ∈ g, u) ∩ v<VAR>hw₂ : w ∈ f<VAR>hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ<VAR>hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<VAR>w : Set τ := (⋂ u ∈ g, u) ∩ v<VAR>hw₂ : w ∈ f<VAR>hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ<VAR>hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ<VAR>hnc : nᶜ ⊆ k \ n ∪ kᶜ<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>c : Set β<VAR>hc₁ : IsCompact c<VAR>n : Set β<VAR>hn₁ : IsOpen n<VAR>hn₂ : ω f ϕ s ⊆ n<VAR>v : Set τ<VAR>hv₁ : v ∈ f<VAR>hv₂ : closure (image2 ϕ v s) ⊆ c<VAR>k : Set β := closure (image2 ϕ v s)<VAR>hk : IsCompact (k \ n)<VAR>j : Set τ → Set β := fun u => (closure (image2 ϕ (u ∩ v) s))ᶜ<VAR>hj₁ : ∀ u ∈ f, IsOpen (j u)<VAR>hj₂ : k \ n ⊆ ⋃ u ∈ f, j u<VAR>g : Set (Set τ)<VAR>hg₁ : ∀ u ∈ g, u ∈ f<VAR>hg₂ : g.Finite<VAR>hg₃ : k \ n ⊆ ⋃ i ∈ g, j i<VAR>w : Set τ := (⋂ u ∈ g, u) ∩ v<VAR>hw₂ : w ∈ f<VAR>hw₃ : k \ n ⊆ (closure (image2 ϕ w s))ᶜ<VAR>hw₄ : kᶜ ⊆ (closure (image2 ϕ w s))ᶜ<VAR>hnc : nᶜ ⊆ k \ n ∪ kᶜ<VAR>hw : closure (image2 ϕ w s) ⊆ n<GOAL>∃ u ∈ f, closure (image2 ϕ u s) ⊆ n
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ PInfty.f n = ((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>K✝ K' : ChainComplex C ℕ<VAR>f : K✝ ⟶ K'<VAR>Δ Δ' Δ'' : SimplexCategory<VAR>inst✝ : HasFiniteCoproducts C<VAR>K : ChainComplex C ℕ<VAR>n : ℕ<GOAL>((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n])) ≫ (P n).f n = ((Γ₀.splitting K).cofan (op [n])).inj (Splitting.IndexSet.id (op [n]))
<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>L : Type u_1<VAR>inst✝ : CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>f : RatFunc K<GOAL>(liftMonoidWithZeroHom φ hφ) f = φ f.num / φ f.denom
<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>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>u : H →L[𝕜] K<GOAL>(∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜) ↔ (adjoint u).comp u = 1
<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>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>u : H →L[𝕜] K<VAR>h : ∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜<VAR>x : H<GOAL>((adjoint u).comp u) x = 1 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>H : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup H<VAR>inst✝⁴ : InnerProductSpace 𝕜 H<VAR>inst✝³ : CompleteSpace H<VAR>K : Type u_6<VAR>inst✝² : NormedAddCommGroup K<VAR>inst✝¹ : InnerProductSpace 𝕜 K<VAR>inst✝ : CompleteSpace K<VAR>u : H →L[𝕜] K<VAR>h : (adjoint u).comp u = 1<GOAL>∀ (x y : H), ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜