ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>κ₁ : Type u_13<VAR>κ₂ : Type u_14<VAR>p₁ : κ₁ → Prop<VAR>s₁ : κ₁ → Set (β × β)<VAR>p₂ : κ₂ → Prop<VAR>s₂ : κ₂ → Set (α × α)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁<VAR>hα : (𝓤 α).HasBasis p₂ s₂<GOAL>(∀ (ib : κ₂), p₂ ib → ∃ ia, p₁ ia ∧ ∀ (a b : β), (a, b) ∈ s₁ ia → ((⇑UniformFun.ofFun ∘ swap F) a, (⇑UniformFun.ofFun ∘ swap F) b) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Semigroup α<VAR>x y z : α<GOAL>((fun x_1 => x * x_1) ∘ fun x => y * x) z = x * y * z
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n✝¹ : ℕ<VAR>a : α<VAR>g : α → α<VAR>hg : LeftInverse g f<VAR>n✝ n : ℕ<VAR>ihn : LeftInverse g^[n] f^[n]<GOAL>LeftInverse g^[n.succ] f^[n.succ]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>m n✝¹ : ℕ<VAR>a : α<VAR>g : α → α<VAR>hg : LeftInverse g f<VAR>n✝ n : ℕ<VAR>ihn : LeftInverse g^[n] f^[n]<GOAL>LeftInverse (g ∘ g^[n]) (f^[n] ∘ f)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → Option β<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ l → f x = g x<GOAL>filterMap f l = filterMap g l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → Option β<VAR>a : α<VAR>l : List α<VAR>ih : (∀ (x : α), x ∈ l → f x = g x) → filterMap f l = filterMap g l<VAR>h : ∀ (x : α), x ∈ a :: l → f x = g x<GOAL>(match f a with | none => filterMap f l | some b => b :: filterMap f l) = match g a with | none => filterMap g l | some b => b :: filterMap g l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → Option β<VAR>a : α<VAR>l : List α<VAR>ih : (∀ (x : α), x ∈ l → f x = g x) → filterMap f l = filterMap g l<VAR>h : ∀ (x : α), x ∈ a :: l → f x = g x<GOAL>(match f a with | none => filterMap g l | some b => b :: filterMap g l) = match g a with | none => filterMap g l | some b => b :: filterMap g l
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidableEq α<VAR>t : Multiset α<GOAL>∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidableEq α<VAR>t✝ : Multiset α<VAR>a : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t<VAR>s : Multiset α<GOAL>filter p (s - a ::ₘ t) = filter p s - filter p (a ::ₘ t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidableEq α<VAR>t✝ : Multiset α<VAR>a : α<VAR>t : Multiset α<VAR>IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t<VAR>s : Multiset α<GOAL>filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)
<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>H : Type u_4<VAR>inst✝⁵ : TopologicalSpace H<VAR>G : Type u_5<VAR>inst✝⁴ : TopologicalSpace G<VAR>I : ModelWithCorners 𝕜 E H<VAR>J : ModelWithCorners 𝕜 F G<VAR>M : Type u_6<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : ChartedSpace H M<VAR>N : Type u_7<VAR>inst✝¹ : TopologicalSpace N<VAR>inst✝ : ChartedSpace G N<VAR>n : ℕ∞<VAR>f : M → N<GOAL>IsLocalDiffeomorph I J n f ↔ ∀ (x : M), IsLocalDiffeomorphAt I J n f x
<VAR>x y : ℂ<GOAL>(cexp x).im = Real.exp x.re * Real.sin x.im
<VAR>x y : ℂ<GOAL>(cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)).im = Real.exp x.re * Real.sin x.im
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoEMetricSpace α<VAR>x y z : α<VAR>s✝ t : Set α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ℝ≥0∞<VAR>h : ∀ (b : β), c ≤ (s b).einfsep<GOAL>c ≤ (univ.pi s).einfsep
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoEMetricSpace α<VAR>x✝ y✝ z : α<VAR>s✝ t : Set α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ℝ≥0∞<VAR>h : ∀ (b : β), c ≤ (s b).einfsep<VAR>x : (i : β) → π i<VAR>hx : x ∈ univ.pi s<VAR>y : (i : β) → π i<VAR>hy : y ∈ univ.pi s<VAR>hxy : x ≠ y<GOAL>c ≤ edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoEMetricSpace α<VAR>x✝ y✝ z : α<VAR>s✝ t : Set α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ℝ≥0∞<VAR>h : ∀ (b : β), c ≤ (s b).einfsep<VAR>x : (i : β) → π i<VAR>hx : ∀ (i : β), x i ∈ s i<VAR>y : (i : β) → π i<VAR>hy : ∀ (i : β), y i ∈ s i<VAR>hxy : x ≠ y<GOAL>c ≤ edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoEMetricSpace α<VAR>x✝ y✝ z : α<VAR>s✝ t : Set α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoEMetricSpace (π b)<VAR>s : (b : β) → Set (π b)<VAR>c : ℝ≥0∞<VAR>h : ∀ (b : β), c ≤ (s b).einfsep<VAR>x : (i : β) → π i<VAR>hx : ∀ (i : β), x i ∈ s i<VAR>y : (i : β) → π i<VAR>hy : ∀ (i : β), y i ∈ s i<VAR>hxy : x ≠ y<VAR>i : β<VAR>hi : x i ≠ y i<GOAL>c ≤ edist x y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p : PrimeSpectrum R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial M<GOAL>support R M = Set.univ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p : PrimeSpectrum R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial M<GOAL>∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>p : PrimeSpectrum R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Nontrivial M<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∀ (x : PrimeSpectrum R), ∃ m, ∀ r ∉ x.asIdeal, ¬r = 0 ∧ ¬m = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>r : R<VAR>x : CliffordAlgebra Q<GOAL>star (r • x) = r • star x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s t : Set σ<GOAL>supported R ∅ = ⊥
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>f g : R'[A]<GOAL>supDegree D (f - g) ≤ supDegree D f ⊔ supDegree D g
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>f g : R'[A]<GOAL>supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>𝓝ˢ s ⊓ 𝓝ˢ t ≤ 𝓝ˢ (s ∩ t)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<GOAL>⨆ x ∈ s, ⨆ x_2 ∈ t, 𝓝 x ⊓ 𝓝 x_2 ≤ ⨆ a ∈ s ∩ t, 𝓝 a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>x : X<VAR>hxs : x ∈ s<VAR>y : X<VAR>hyt : y ∈ t<GOAL>𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>x : X<VAR>hxs : x ∈ s<VAR>hyt : x ∈ t<GOAL>𝓝 x ⊓ 𝓝 x ≤ ⨆ a ∈ s ∩ t, 𝓝 a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>x : X<VAR>hxs : x ∈ s<VAR>y : X<VAR>hyt : y ∈ t<VAR>hne : x ≠ y<GOAL>𝓝 x ⊓ 𝓝 y ≤ ⨆ a ∈ s ∩ t, 𝓝 a
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝ : Fintype V<VAR>h : M.IsPerfectMatching<GOAL>Even (Fintype.card V)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>n m l : ℕ<GOAL>range n = ∅ ↔ n = 0
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if h : { byteIdx := utf8Len l } < { byteIdx := utf8Len l + utf8Len (c :: m) } then if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then let_fun this := ⋯; Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) else { byteIdx := utf8Len l } else { byteIdx := utf8Len l }) = { byteIdx := utf8Len l + utf8Len (match p c with | true => c :: List.takeWhile p m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if p ({ data := l ++ c :: m ++ r }.get { byteIdx := utf8Len l }) = true then let_fun this := ⋯; Substring.takeWhileAux { data := l ++ c :: m ++ r } { byteIdx := utf8Len l + utf8Len (c :: m) } p ({ data := l ++ c :: m ++ r }.next { byteIdx := utf8Len l }) else { byteIdx := utf8Len l }) = { byteIdx := utf8Len l + utf8Len (match p c with | true => c :: List.takeWhile p m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>(if p c = true then Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p { byteIdx := utf8Len l + c.utf8Size } else { byteIdx := utf8Len l }) = { byteIdx := utf8Len l + utf8Len (match p c with | true => c :: List.takeWhile p m | false => []) }
<VAR>p : Char → Bool<VAR>l : List Char<VAR>c : Char<VAR>m r : List Char<GOAL>Substring.takeWhileAux { data := l ++ c :: (m ++ r) } { byteIdx := utf8Len l + (utf8Len m + c.utf8Size) } p { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l + (utf8Len (List.takeWhile p m) + c.utf8Size) }
<VAR>n : ℕ<GOAL>(hermite n).leadingCoeff = 1
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<VAR>I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<VAR>I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}<VAR>I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<VAR>I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}<VAR>I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}<VAR>I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<VAR>I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}<VAR>I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}<VAR>I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)}<VAR>this : GromovHausdorff.candidatesB X Y = (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩ ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩ ⋂ x, {f | f (x, x) = 0}) ∩ ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)}<GOAL>IsClosed (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<VAR>I1 : ∀ (x y : X), IsClosed {f | f (inl x, inl y) = dist x y}<VAR>I2 : ∀ (x y : Y), IsClosed {f | f (inr x, inr y) = dist x y}<VAR>I3 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) = f (y, x)}<VAR>I4 : ∀ (x y z : X ⊕ Y), IsClosed {f | f (x, z) ≤ f (x, y) + f (y, z)}<VAR>I5 : ∀ (x : X ⊕ Y), IsClosed {f | f (x, x) = 0}<VAR>I6 : ∀ (x y : X ⊕ Y), IsClosed {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)}<VAR>this : GromovHausdorff.candidatesB X Y = (((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩ ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩ ⋂ x, {f | f (x, x) = 0}) ∩ ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)}<GOAL>IsClosed ((((((⋂ x, ⋂ y, {f | f (inl x, inl y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (inr x, inr y) = dist x y}) ∩ ⋂ x, ⋂ y, {f | f (x, y) = f (y, x)}) ∩ ⋂ x, ⋂ y, ⋂ z, {f | f (x, z) ≤ f (x, y) + f (y, z)}) ∩ ⋂ x, {f | f (x, x) = 0}) ∩ ⋂ x, ⋂ y, {f | f (x, y) ≤ ↑(GromovHausdorff.maxVar X Y)})
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : (𝓝[≠] x).NeBot<VAR>y : X<GOAL>y ∈ closure {x}ᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>y : X<VAR>inst✝ : (𝓝[≠] y).NeBot<GOAL>y ∈ closure {y}ᶜ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x✝ : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : (𝓝[≠] x).NeBot<VAR>y : X<VAR>hne : y ≠ x<GOAL>y ∈ closure {x}ᶜ
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<GOAL>OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>b : OrthonormalBasis { x // x ∈ Classical.choose ⋯ } 𝕜 E := Classical.choose ⋯<GOAL>OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝¹⁰ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : InnerProductSpace ℝ F'<VAR>inst✝¹ : Fintype ι<VAR>v : Set E<VAR>A : ι → Submodule 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>b : OrthonormalBasis { x // x ∈ Classical.choose ⋯ } 𝕜 E := Classical.choose ⋯<GOAL>OrthonormalBasis (Fin (Fintype.card { x // x ∈ Classical.choose ⋯ })) 𝕜 E
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(↑s).toSeq = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>↑(↑s).toSeq = ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>↑(↑s).toSeq n = ↑s n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>((↑s).get? n).get = ↑s n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>↑s n ∈ (↑s).get? n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>↑s n ∈ Computation.pure (s.get? n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<VAR>hF : ∀ i ∈ s, padicNorm p (F i) < t<VAR>ht : 0 < t<GOAL>padicNorm p (∑ i ∈ s, F i) < t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>ht : 0 < t<VAR>hF : ∀ i ∈ ∅, padicNorm p (F i) < t<GOAL>padicNorm p (∑ i ∈ ∅, F i) < t
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>α : Type u_1<VAR>F : α → ℚ<VAR>t : ℚ<VAR>s : Finset α<VAR>hF : ∀ i ∈ s, padicNorm p (F i) < t<VAR>ht : 0 < t<VAR>hs : s.Nonempty<GOAL>padicNorm p (∑ i ∈ s, F i) < t
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle y (y - x)).tan = ‖x‖ / ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle y (y - x)).sign = 1<GOAL>(o.oangle y (y - x)).tan = ‖x‖ / ‖y‖
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>hf : Injective fun a => f a b<GOAL>image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<VAR>b : β<GOAL>∏ x ∈ s, update f i b x = b * ∏ x ∈ s \ {i}, f x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>i : α<VAR>h : i ∈ s<VAR>f : α → β<VAR>b : β<GOAL>(∏ x ∈ s ∩ {i}, b) * ∏ x ∈ s \ {i}, f x = b * ∏ x ∈ s \ {i}, f x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>I.polynomialQuotientEquivQuotientPolynomial.symm ((Quotient.mk (map C I)) f) = Polynomial.map (Quotient.mk I) f
<VAR>a b n : ℕ<GOAL>¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : Semiring R<VAR>A₁ : Matrix m₁ n R<VAR>A₂ : Matrix m₂ n R<VAR>B : Matrix n m R<GOAL>A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<GOAL>H.index * Nat.card ↥H = Nat.card G
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : G × G → CoeSort.coe A<GOAL>f ∈ twoCocycles A ↔ ∀ (g h j : G), f (g * h, j) + f (g, h) = (A.ρ g) (f (h, j)) + f (g, h * j)
<GOAL>|rexp 1 - 2244083 / 825552| ≤ 1 / 10 ^ 10