ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<VAR>bdd : BddAbove (range fun x => f x + c)<VAR>hs : ℵ₀ ≤ ⨆ i, f i<GOAL>(⨆ i, f i) + c ≤ ⨆ i, f i + c
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>hf : BddAbove (range f)<VAR>c : Cardinal.{v}<VAR>this : ∀ (i : ι), f i + c ≤ (⨆ i, f i) + c<VAR>bdd : BddAbove (range fun x => f x + c)<VAR>hs : ℵ₀ ≤ ⨆ i, f i<GOAL>⨆ i, f i ≤ ⨆ i, f i + c ∧ c ≤ ⨆ i, f i + c
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<VAR>x✝¹ x✝ : G<VAR>ha : x✝¹ ∈ A<VAR>hb : x✝ ∈ B<VAR>k : x✝¹ ≠ a0 ∨ x✝ ≠ b0<GOAL>x✝¹ * x✝ ≠ a0 * b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Mul G<VAR>inst✝ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>h : UniqueMul A B a0 b0<VAR>x✝¹ x✝ : G<VAR>ha : x✝¹ ∈ A<VAR>hb : x✝ ∈ B<VAR>k : x✝¹ * x✝ = a0 * b0<GOAL>x✝¹ = a0 ∧ x✝ = b0
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>y < -x ↔ x < -y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<GOAL>EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : b ≤ a<GOAL>EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>a b : ℝ<VAR>h : a < b<GOAL>EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>h : ∀ (v : E), ⟪x, v⟫_𝕜 = ⟪y, v⟫_𝕜<GOAL>x = y
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Add R<VAR>inst✝ : BoundedAdd R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Add R<VAR>inst✝ : BoundedAdd R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Add R<VAR>inst✝ : BoundedAdd R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C<GOAL>∀ (x y : X), dist ((f + g) x) ((f + g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Add R<VAR>inst✝ : BoundedAdd R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f + Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f + Set.range g → dist x y ≤ C<VAR>x y : X<GOAL>dist ((f + g) x) ((f + g) y) ≤ C
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : MulOneClass M<VAR>inst✝ : ContinuousMul M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 1<GOAL>∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : MulOneClass M<VAR>inst✝ : ContinuousMul M<VAR>s : Set M<VAR>hs : s ∈ 𝓝 1<VAR>this : (fun a => a.1 * a.2) ⁻¹' s ∈ 𝓝 (1, 1)<GOAL>∃ V, IsOpen V ∧ 1 ∈ V ∧ ∀ v ∈ V, ∀ w ∈ V, v * w ∈ s
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>f g : ℕ → α<VAR>h : partialSups f ≤ partialSups g<GOAL>⨆ n, f n ≤ ⨆ n, g n
<VAR>α : Type u_1<VAR>inst✝ : CompleteLattice α<VAR>f g : ℕ → α<VAR>h : partialSups f ≤ partialSups g<GOAL>⨆ n, (partialSups f) n ≤ ⨆ n, (partialSups g) n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring S<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>v✝ : α → M<VAR>v' : α' → M'<VAR>inst✝ : Unique α<VAR>l : α →₀ R<VAR>v : α → M<GOAL>(Finsupp.total α M R v) l = l default • v default
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>i : V<GOAL>(adjMatrix α G * adjMatrix α G) i i = ↑(G.degree i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>¬IsMin a ↔ ∃ b, b < a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>α : Type u_8<VAR>inst✝ : Monoid α<GOAL>(fun x => (↑x, op ↑x⁻¹)) 1 = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>α : Type u_8<VAR>inst✝ : Monoid α<VAR>x y : αˣ<GOAL>{ toFun := fun x => (↑x, op ↑x⁻¹), map_one' := ⋯ }.toFun (x * y) = { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := ⋯ }.toFun x * { toFun := fun x => (↑x, op ↑x⁻¹), map_one' := ⋯ }.toFun y
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n✝ N : ℕ<VAR>φ : MvPolynomial (Fin (N + 1)) R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>d : Fin N →₀ ℕ<VAR>hd : coeff d (((finSuccEquiv R N) φ).coeff i) ≠ 0<GOAL>(weight 1) d = j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n✝ N : ℕ<VAR>φ : MvPolynomial (Fin (N + 1)) R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>d : Fin N →₀ ℕ<VAR>hd : coeff (cons i d) φ ≠ 0<GOAL>(weight 1) d = j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n✝ N : ℕ<VAR>φ : MvPolynomial (Fin (N + 1)) R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>d : Fin N →₀ ℕ<VAR>hd : coeff (cons i d) φ ≠ 0<VAR>h' : (weight 1) (cons i d) = i + j<GOAL>(weight 1) d = j
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ✝ ψ : MvPolynomial σ R<VAR>m n✝ N : ℕ<VAR>φ : MvPolynomial (Fin (N + 1)) R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<VAR>d : Fin N →₀ ℕ<VAR>hd : coeff (cons i d) φ ≠ 0<VAR>h' : (d.sum fun x e => e) = j<GOAL>(d.sum fun i c => c) = j
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hf : Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, (μ[f|m]) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hf : Integrable f μ<VAR>hs : MeasurableSet s<GOAL>∫ (x : α) in s, ↑↑(condexpL1 hm μ f) x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝² : μ.InnerRegularCompactLTTop<VAR>inst✝¹ : R1Space α<VAR>inst✝ : BorelSpace α<VAR>A : Set α<VAR>hA : MeasurableSet A<VAR>h'A : μ A ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>K : Set α<VAR>hKA : K ⊆ A<VAR>hK : IsCompact K<VAR>hμK : μ A < μ K + ε<GOAL>μ A < μ (closure K) + ε
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁵ : SetLike σ A<VAR>inst✝⁴ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝³ : GradedRing 𝒜<VAR>b : A<VAR>n i : ι<VAR>inst✝² : Sub ι<VAR>inst✝¹ : OrderedSub ι<VAR>inst✝ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>h : i ≤ n<VAR>a : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (↑a * b)) n) = ↑a * ↑(((decompose 𝒜) b) (n - i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>f : CompleteLatticeHom α β<VAR>L : CompleteSublattice α<VAR>a b : ↥L<GOAL>Disjoint a b ↔ Disjoint ↑a ↑b
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsGalois A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ : Aut B<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a : ↑(F.obj A)<GOAL>∃ a, autMap f a = σ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsGalois A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ : Aut B<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a a' : ↑(F.obj A)<VAR>ha' : F.map f a' = F.map σ.hom (F.map f a)<GOAL>∃ a, autMap f a = σ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsGalois A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ : Aut B<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a a' : ↑(F.obj A)<VAR>ha' : F.map f a' = F.map σ.hom (F.map f a)<VAR>τ : Aut A<VAR>hτ : F.map τ.hom a = a'<GOAL>∃ a, autMap f a = σ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsGalois A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ : Aut B<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a a' : ↑(F.obj A)<VAR>ha' : F.map f a' = F.map σ.hom (F.map f a)<VAR>τ : Aut A<VAR>hτ : F.map τ.hom a = a'<GOAL>autMap f τ = σ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsGalois A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ : Aut B<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a a' : ↑(F.obj A)<VAR>ha' : F.map f a' = F.map σ.hom (F.map f a)<VAR>τ : Aut A<VAR>hτ : F.map τ.hom a = a'<GOAL>(fun f_1 => F.map f_1.hom (F.map f a)) (autMap f τ) = (fun f_1 => F.map f_1.hom (F.map f a)) σ
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>x : E<VAR>hf : ContinuousAt f x<GOAL>oscillation f x = 0
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>x : E<VAR>hf : ContinuousWithinAt f univ x<GOAL>oscillation f x = 0
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : AlexandrovDiscrete α<VAR>S✝ : Set (Set α)<VAR>f : ι → Set α<VAR>S : Set (Set α)<GOAL>closure (⋃₀ S) = ⋃ s ∈ S, closure s
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>inst✝ : Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>x : ↑(F.obj X)<GOAL>F.map (CategoryTheory.PreGaloisCategory.selfProdProj u x) a = x
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F<VAR>X A : C<VAR>inst✝¹ : IsConnected A<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>inst✝ : Mono u<VAR>a : ↑(F.obj A)<VAR>h : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>x : ↑(F.obj X)<GOAL>F.map (Pi.π (fun x => X) x) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = x
<VAR>a b c : Ordinal.{u_1}<VAR>h₁ : a < ω ^ b<VAR>h₂ : ω ^ b ≤ c<GOAL>a + c = c
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝¹⁴ : TopologicalSpace G<VAR>inst✝¹³ : TopologicalSpace X<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : TopologicalGroup G<VAR>inst✝¹⁰ : MulAction G X<VAR>inst✝⁹ : SigmaCompactSpace G<VAR>inst✝⁸ : BaireSpace X<VAR>inst✝⁷ : T2Space X<VAR>inst✝⁶ : ContinuousSMul G X<VAR>inst✝⁵ : IsPretransitive G X<VAR>H : Type u_3<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : BaireSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : ContinuousMul H<VAR>f : G →* H<VAR>hf : Surjective ⇑f<VAR>h'f : Continuous ⇑f<VAR>A : MulAction G H := MulAction.compHom H f<GOAL>IsOpenMap ⇑f
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝¹⁴ : TopologicalSpace G<VAR>inst✝¹³ : TopologicalSpace X<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : TopologicalGroup G<VAR>inst✝¹⁰ : MulAction G X<VAR>inst✝⁹ : SigmaCompactSpace G<VAR>inst✝⁸ : BaireSpace X<VAR>inst✝⁷ : T2Space X<VAR>inst✝⁶ : ContinuousSMul G X<VAR>inst✝⁵ : IsPretransitive G X<VAR>H : Type u_3<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : BaireSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : ContinuousMul H<VAR>f : G →* H<VAR>hf : Surjective ⇑f<VAR>h'f : Continuous ⇑f<VAR>A : MulAction G H := MulAction.compHom H f<VAR>this : ContinuousSMul G H<GOAL>IsOpenMap ⇑f
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝¹⁴ : TopologicalSpace G<VAR>inst✝¹³ : TopologicalSpace X<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : TopologicalGroup G<VAR>inst✝¹⁰ : MulAction G X<VAR>inst✝⁹ : SigmaCompactSpace G<VAR>inst✝⁸ : BaireSpace X<VAR>inst✝⁷ : T2Space X<VAR>inst✝⁶ : ContinuousSMul G X<VAR>inst✝⁵ : IsPretransitive G X<VAR>H : Type u_3<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : BaireSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : ContinuousMul H<VAR>f : G →* H<VAR>hf : Surjective ⇑f<VAR>h'f : Continuous ⇑f<VAR>A : MulAction G H := MulAction.compHom H f<VAR>this✝ : ContinuousSMul G H<VAR>this : IsPretransitive G H<GOAL>IsOpenMap ⇑f
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝¹⁴ : TopologicalSpace G<VAR>inst✝¹³ : TopologicalSpace X<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : TopologicalGroup G<VAR>inst✝¹⁰ : MulAction G X<VAR>inst✝⁹ : SigmaCompactSpace G<VAR>inst✝⁸ : BaireSpace X<VAR>inst✝⁷ : T2Space X<VAR>inst✝⁶ : ContinuousSMul G X<VAR>inst✝⁵ : IsPretransitive G X<VAR>H : Type u_3<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : BaireSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : ContinuousMul H<VAR>f : G →* H<VAR>hf : Surjective ⇑f<VAR>h'f : Continuous ⇑f<VAR>A : MulAction G H := MulAction.compHom H f<VAR>this✝¹ : ContinuousSMul G H<VAR>this✝ : IsPretransitive G H<VAR>this : ⇑f = fun g => g • 1<GOAL>IsOpenMap ⇑f
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝¹⁴ : TopologicalSpace G<VAR>inst✝¹³ : TopologicalSpace X<VAR>inst✝¹² : Group G<VAR>inst✝¹¹ : TopologicalGroup G<VAR>inst✝¹⁰ : MulAction G X<VAR>inst✝⁹ : SigmaCompactSpace G<VAR>inst✝⁸ : BaireSpace X<VAR>inst✝⁷ : T2Space X<VAR>inst✝⁶ : ContinuousSMul G X<VAR>inst✝⁵ : IsPretransitive G X<VAR>H : Type u_3<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : BaireSpace H<VAR>inst✝¹ : T2Space H<VAR>inst✝ : ContinuousMul H<VAR>f : G →* H<VAR>hf : Surjective ⇑f<VAR>h'f : Continuous ⇑f<VAR>A : MulAction G H := MulAction.compHom H f<VAR>this✝¹ : ContinuousSMul G H<VAR>this✝ : IsPretransitive G H<VAR>this : ⇑f = fun g => g • 1<GOAL>IsOpenMap fun g => g • 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : δ < 1<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : δ < 1<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs : ∅ ⊆ s₁<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑∅.card<GOAL>|↑(edgeDensity r ∅ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht : ∅ ⊆ t₁<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑∅.card<GOAL>|↑(edgeDensity r s₂ ∅) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<GOAL>|↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 2 * δ - δ ^ 2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<VAR>hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)<GOAL>↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - (1 - δ) * (1 - δ)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<VAR>hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)<GOAL>↑(1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card)) ≤ 1 - (1 - δ) * (1 - δ)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<VAR>hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)<GOAL>1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) ≤ 1 - (1 - δ) * (1 - δ)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<VAR>hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)<VAR>h₁ : s₁.Nonempty<GOAL>1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) ≤ 1 - (1 - δ) * (1 - δ)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>hs : s₂ ⊆ s₁<VAR>ht : t₂ ⊆ t₁<VAR>hδ₀ : 0 ≤ δ<VAR>hδ₁ : 0 < 1 - δ<VAR>hs₂ : (1 - δ) * ↑s₁.card ≤ ↑s₂.card<VAR>ht₂ : (1 - δ) * ↑t₁.card ≤ ↑t₂.card<VAR>hδ' : 0 ≤ 2 * δ - δ ^ 2<VAR>hs₂' : s₂.Nonempty<VAR>ht₂' : t₂.Nonempty<VAR>hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)<VAR>h₁ : s₁.Nonempty<VAR>h₂ : t₁.Nonempty<GOAL>1 - ↑s₂.card / ↑s₁.card * (↑t₂.card / ↑t₁.card) ≤ 1 - (1 - δ) * (1 - δ)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Precoherent D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>B₁ B₂ : C<VAR>f : B₂ ⟶ B₁<VAR>α : Type<VAR>x✝¹ : Finite α<VAR>X₁ : α → C<VAR>π₁ : (a : α) → X₁ a ⟶ B₁<VAR>x✝ : EffectiveEpiFamily X₁ π₁<GOAL>∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{?u.230, u_2} D<VAR>F : C ⥤ D<VAR>inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies<VAR>inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies<VAR>inst✝³ : F.EffectivelyEnough<VAR>inst✝² : Precoherent D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>B₁ B₂ : C<VAR>f : B₂ ⟶ B₁<VAR>α : Type<VAR>x✝¹ : Finite α<VAR>X₁ : α → C<VAR>π₁ : (a : α) → X₁ a ⟶ B₁<VAR>x✝ : EffectiveEpiFamily X₁ π₁<VAR>β : Type<VAR>w✝ : Finite β<VAR>Y₂ : β → D<VAR>τ₂ : (b : β) → Y₂ b ⟶ F.obj B₂<VAR>H : EffectiveEpiFamily Y₂ τ₂<VAR>i : β → α<VAR>ι : (b : β) → Y₂ b ⟶ F.obj (X₁ (i b))<VAR>hh : ∀ (b : β), ι b ≫ F.map (π₁ (i b)) = τ₂ b ≫ F.map f<GOAL>∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f