ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝ : tα ⊆ univ<VAR>hfin : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝ : Fintype ↑tα<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<VAR>F : β → β<VAR>hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂<GOAL>∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<VAR>F : β → β<VAR>hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂<GOAL>∀ (x y : ↑A), (fun f a => ⟨F (↑f ↑a), ⋯⟩) x = (fun f a => ⟨F (↑f ↑a), ⋯⟩) y → dist ↑x ↑y < ε
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f✝ g✝ : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<VAR>F : β → β<VAR>hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂<VAR>f : α →ᵇ β<VAR>hf : f ∈ A<VAR>g : α →ᵇ β<VAR>hg : g ∈ A<VAR>f_eq_g : (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩<GOAL>dist ↑⟨f, hf⟩ ↑⟨g, hg⟩ < ε
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f✝ g✝ : α →ᵇ β<VAR>x✝ : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<VAR>F : β → β<VAR>hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂<VAR>f : α →ᵇ β<VAR>hf : f ∈ A<VAR>g : α →ᵇ β<VAR>hg : g ∈ A<VAR>f_eq_g : (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩<VAR>x : α<GOAL>dist (↑⟨f, hf⟩ x) (↑⟨g, hg⟩ x) ≤ ε₁
<VAR>F✝ : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : CompactSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>f✝ g✝ : α →ᵇ β<VAR>x✝ : α<VAR>C : ℝ<VAR>inst✝ : CompactSpace β<VAR>A : Set (α →ᵇ β)<VAR>closed : IsClosed A<VAR>H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>ε₁ : ℝ<VAR>ε₁0 : 0 < ε₁<VAR>εε₁ : ε₁ < ε<VAR>ε₂ : ℝ := ε₁ / 2 / 2<VAR>ε₂0 : ε₂ > 0<VAR>U : α → Set α<VAR>hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂<VAR>tα : Set α<VAR>left✝¹ : tα ⊆ univ<VAR>hfin✝ : tα.Finite<VAR>htα : univ ⊆ ⋃ x ∈ tα, U x<VAR>val✝¹ : Fintype ↑tα<VAR>tβ : Set β<VAR>left✝ : tβ ⊆ univ<VAR>hfin : tβ.Finite<VAR>htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂<VAR>val✝ : Fintype ↑tβ<VAR>F : β → β<VAR>hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂<VAR>f : α →ᵇ β<VAR>hf : f ∈ A<VAR>g : α →ᵇ β<VAR>hg : g ∈ A<VAR>f_eq_g : (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a => ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩<VAR>x x' : α<VAR>x'tα : x' ∈ tα<VAR>hx' : x ∈ U x'<GOAL>dist (↑⟨f, hf⟩ x) (↑⟨g, hg⟩ x) ≤ ε₁
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<GOAL>thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>hε : ε ≤ 0<GOAL>thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>hε : 0 ≤ ε<GOAL>thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>x : α<GOAL>x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>x : α<GOAL>(∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) → infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s✝ t : Set α<VAR>x✝ : α<VAR>ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>s : Set α<VAR>hε : 0 ≤ ε<VAR>x y : α<VAR>hy : infEdist y s ≤ ENNReal.ofReal δ<VAR>hxy : edist x y < ENNReal.ofReal ε<GOAL>infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>hl : (i :: l).Nodup<VAR>hj : j ∈ l<VAR>v : TProd α (i :: l)<GOAL>v.elim ⋯ = TProd.elim v.2 hj
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>i j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>hl : (i :: l).Nodup<VAR>hj : j ∈ l<VAR>v : TProd α (i :: l)<GOAL>j ≠ i
<VAR>ι : Type u<VAR>α : ι → Type v<VAR>j : ι<VAR>l : List ι<VAR>f : (i : ι) → α i<VAR>inst✝ : DecidableEq ι<VAR>hj : j ∈ l<VAR>hl : (j :: l).Nodup<VAR>v : TProd α (j :: l)<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>x : β<GOAL>x ∈ r.image ∅ ↔ x ∈ ∅
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>φ : M →[L] N<VAR>S : L.Substructure N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<VAR>hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S<GOAL>funMap f x ∈ ⇑φ ⁻¹' ↑S
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S✝ : L.Substructure M<VAR>s : Set M<VAR>φ : M →[L] N<VAR>S : L.Substructure N<VAR>n : ℕ<VAR>f : L.Functions n<VAR>x : Fin n → M<VAR>hx : ∀ (i : Fin n), x i ∈ ⇑φ ⁻¹' ↑S<GOAL>funMap f (⇑φ ∘ x) ∈ ↑S
<VAR>α β γ : Type u<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : CommApplicative F<VAR>inst✝ : CommApplicative G<VAR>g : α → G β<VAR>h : β → γ<VAR>s : Finset α<GOAL>Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val = Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
<VAR>α β γ : Type u<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : CommApplicative F<VAR>inst✝ : CommApplicative G<VAR>g : α → G β<VAR>h : β → γ<VAR>s : Finset α<GOAL>(Multiset.toFinset ∘ Functor.map h) <$> Multiset.traverse g s.val = Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>((foldr Q (changeFormAux Q' B) ⋯) (((foldr Q (changeFormAux Q' B) ⋯) 1) x)) ((ι Q) m) = (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q Q' Q'' : QuadraticForm R M<VAR>B B' : BilinForm R M<VAR>h : BilinMap.toQuadraticMap B = Q' - Q<VAR>h' : BilinMap.toQuadraticMap B' = Q'' - Q'<VAR>m : M<VAR>x : CliffordAlgebra Q<GOAL>((changeFormAux Q' B) m) (((foldr Q (changeFormAux Q' B) ⋯) 1) x) = (ι Q') m * (changeForm h) x - (contractLeft (B m)) ((changeForm h) x)
<VAR>s : ℂ<VAR>hs : s ≠ 0<GOAL>riemannZeta s = completedRiemannZeta s / s.Gammaℝ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>b \ (a ⊓ b) = b \ a
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp✝ : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>hp : p ≠ ⊤<VAR>f : WithLp p (α × β)<GOAL>↑‖f‖₊ = ↑((‖f.1‖₊ ^ p.toReal + ‖f.2‖₊ ^ p.toReal) ^ (1 / p.toReal))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a b c d : α<VAR>n : ℕ<GOAL>(a * b) ^ ↑n = a ^ ↑n * b ^ ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionCommMonoid α<VAR>a b c d : α<VAR>n : ℕ<GOAL>(a * b) ^ Int.negSucc n = a ^ Int.negSucc n * b ^ Int.negSucc n
<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>B : Type u<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsScalarTower R A B<VAR>inst✝² : FormallyUnramified R B<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra A Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[A] Q<VAR>e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂<VAR>this : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>B : Type u<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsScalarTower R A B<VAR>inst✝² : FormallyUnramified R B<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra A Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[A] Q<VAR>e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂<VAR>this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra<VAR>this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl<GOAL>f₁ = f₂
<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>B : Type u<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsScalarTower R A B<VAR>inst✝² : FormallyUnramified R B<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra A Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[A] Q<VAR>e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂<VAR>this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra<VAR>this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl<GOAL>AlgHom.restrictScalars R f₁ = AlgHom.restrictScalars R f₂
<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>B : Type u<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsScalarTower R A B<VAR>inst✝² : FormallyUnramified R B<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra A Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[A] Q<VAR>e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂<VAR>this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra<VAR>this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl<GOAL>∀ (x : B), (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)
<VAR>R : Type u<VAR>inst✝⁹ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>B : Type u<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : IsScalarTower R A B<VAR>inst✝² : FormallyUnramified R B<VAR>Q : Type u<VAR>inst✝¹ : CommRing Q<VAR>inst✝ : Algebra A Q<VAR>I : Ideal Q<VAR>e : I ^ 2 = ⊥<VAR>f₁ f₂ : B →ₐ[A] Q<VAR>e' : (Ideal.Quotient.mkₐ A I).comp f₁ = (Ideal.Quotient.mkₐ A I).comp f₂<VAR>this✝ : Algebra R Q := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra<VAR>this : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl<VAR>x : B<GOAL>(Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₁) x) = (Ideal.Quotient.mk I) ((AlgHom.restrictScalars R f₂) x)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<GOAL>Function.Injective ⇑((forget₂ C Ab).map S.f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>hS : S.ShortExact<GOAL>Mono S.f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v✝ : HeightOneSpectrum R<VAR>c : R_hat R K<VAR>v : HeightOneSpectrum R<GOAL>(fun v => ↑↑c v) v ∈ adicCompletionIntegers K v
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>Differentiable 𝕜 f ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), Differentiable 𝕜 fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) ↔ ∀ (i : ι), Differentiable 𝕜 fun x => f x i
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x✝¹ x✝ : α<GOAL>Setoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>x✝¹ x✝ : α<GOAL>(fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
<VAR>F : Type u_1<VAR>R✝ : Type u_2<VAR>S : Type u_3<VAR>x✝ y : R✝<VAR>r : ℝ<VAR>R : Type u_4<VAR>inst✝ : Ring R<VAR>x : ℤ<VAR>f : MulRingNorm R<GOAL>f ↑x.natAbs = f ↑x
<VAR>m n : ℕ<GOAL>bits 1 = [true]
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝ : S.HasLeftHomology<GOAL>S.liftCycles k hk ≫ h.cyclesIso.hom = h.liftK k hk
<VAR>m n a b c d : ℕ<VAR>hmc : m.gcd c = 1<VAR>h : a * c ≡ b * c [MOD m]<GOAL>c * a ≡ c * b [MOD m]
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a b : ℕ<VAR>h : a ≤ b<GOAL>↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a b : ℕ<VAR>h : a ≤ b<VAR>this : ∀ {n : ℕ}, ↑n ! ≠ 0<GOAL>↑(b.choose a) = ↑b ! / (↑a ! * ↑(b - a)!)
<VAR>K : Type u_1<VAR>inst✝¹ : DivisionRing K<VAR>inst✝ : CharZero K<VAR>a b : ℕ<VAR>h : a ≤ b<VAR>this : ∀ {n : ℕ}, ↑n ! ≠ 0<GOAL>↑(b.choose a) * (↑a ! * ↑(b - a)!) = ↑b !
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>inst✝ : CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>y✝ : E<VAR>hy : y✝ ∈ EMetric.ball 0 p.radius<GOAL>HasSum (fun n => (p n) fun x => y✝) (p.sum (0 + y✝))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>inst✝ : CompleteSpace F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>h : 0 < p.radius<VAR>y✝ : E<VAR>hy : y✝ ∈ EMetric.ball 0 p.radius<GOAL>HasSum (fun n => (p n) fun x => y✝) (p.sum y✝)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Ring α<GOAL>IsDomain α ↔ NoZeroDivisors α ∧ Nontrivial α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t✝ s t : Set α<GOAL>s =ᶠ[ae μ] t ↔ μ (s \ t) = 0 ∧ μ (t \ s) = 0
<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>s s' t : Set α<VAR>hs : IsOpen s<VAR>hs' : IsOpen s'<VAR>ht : s ∩ frontier t = s' ∩ frontier t<VAR>x : α<VAR>hx : x ∈ frontier t<GOAL>x ∈ s ↔ x ∈ s'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : OrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>l✝ : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>A : Set E<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>w : E<VAR>hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<GOAL>∃ l_1 a, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∧ a ≤ l_1 x}
<VAR>M₀ : Type u_1<VAR>G₀ : Type u_2<VAR>M₀' : Type u_3<VAR>G₀' : Type u_4<VAR>inst✝⁴ : Mul M₀<VAR>inst✝³ : Zero M₀<VAR>inst✝² : Mul M₀'<VAR>inst✝¹ : Zero M₀'<VAR>f : M₀ → M₀'<VAR>hf : Injective f<VAR>zero : f 0 = 0<VAR>mul : ∀ (x y : M₀), f (x * y) = f x * f y<VAR>inst✝ : IsRightCancelMulZero M₀'<VAR>a✝ b✝ c✝ : M₀<VAR>Hne : b✝ ≠ 0<VAR>He : a✝ * b✝ = c✝ * b✝<VAR>this : f a✝ * f b✝ = f c✝ * f b✝<GOAL>a✝ = c✝
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>a : R<VAR>h : a ≠ 0<GOAL>(∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧ Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>a : R<VAR>h : a ≠ 0<GOAL>(∀ b ∈ Classical.choose ⋯, Irreducible b) ∧ Associated (Classical.choose ⋯).prod a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Antitone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<GOAL>CauchySeq fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>b : ℝ<VAR>f : ℕ → ℝ<VAR>z : ℕ → E<VAR>hfa : Antitone f<VAR>hf0 : Tendsto f atTop (𝓝 0)<GOAL>CauchySeq fun n => ∑ x ∈ Finset.range n, f x * (-1) ^ x
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid M✝<VAR>inst✝¹⁵ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : CommRing R₁<VAR>inst✝¹³ : AddCommGroup M₁<VAR>inst✝¹² : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹¹ : CommSemiring R₂<VAR>inst✝¹⁰ : AddCommMonoid M₂<VAR>inst✝⁹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁸ : CommRing R₃<VAR>inst✝⁷ : AddCommGroup M₃<VAR>inst✝⁶ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype o<VAR>inst✝ : DecidableEq n<VAR>b : Basis n R₂ M₂<VAR>M : Matrix n n R₂<VAR>i✝¹ i✝ : n<GOAL>(((toBilin (Pi.basisFun R₂ n)) M ∘ₗ single i✝¹) 1 ∘ₗ single i✝) 1 = ((toBilin' M ∘ₗ single i✝¹) 1 ∘ₗ single i✝) 1