ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : QuotientMap g<VAR>hf : QuotientMap f<GOAL>inst✝ = coinduced (g ∘ f) inst✝²
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a✝ a' : α<VAR>b✝ : M<VAR>f : α →₀ M<VAR>a : α<VAR>x✝ : ∃ b, f = single a b<VAR>b : M<VAR>hb : f = single a b<GOAL>f.support ⊆ {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>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>f : M →ₙ* N × P<VAR>x : M<GOAL>(((fst N P).comp f).prod ((snd N P).comp f)) x = f x
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} / ball y δ = ball (x / y) δ
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>u : ℤˣ<VAR>a : ↥(toSubgroup A B u)<GOAL>↑((toSubgroupEquiv φ (-u)) ((toSubgroupEquiv φ u) a)) = ↑a
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥(toSubgroup A B 1)<GOAL>↑((toSubgroupEquiv φ (-1)) ((toSubgroupEquiv φ 1) a)) = ↑a
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>a : ↥(toSubgroup A B (-1))<GOAL>↑((toSubgroupEquiv φ (- -1)) ((toSubgroupEquiv φ (-1)) a)) = ↑a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s a : ℂ<GOAL>mellin (fun t => ↑t ^ a • f t) s = mellin f (s + a)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s a : ℂ<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (s - 1) • (fun t => ↑t ^ a • f t) t = ↑t ^ (s + a - 1) • f t
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>p : P<VAR>hp : p ∈ ↑s<VAR>this : Nonempty ↥s<GOAL>IsConnected {y | s.SSameSide x y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>p : P<VAR>hp : p ∈ ↑s<VAR>this : Nonempty ↥s<GOAL>IsConnected ((fun x_1 => x_1.1 • (x -ᵥ p) +ᵥ x_1.2) '' Set.Ioi 0 ×ˢ ↑s)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : AffineSubspace ℝ P<VAR>x : P<VAR>hx : x ∉ s<VAR>p : P<VAR>hp : p ∈ ↑s<VAR>this : Nonempty ↥s<GOAL>ConnectedSpace ↑↑s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>α : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : SetLike S R<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid ι<VAR>A : ι → S<VAR>inst✝ : GradedMonoid A<VAR>fι : α → ι<VAR>fA : (a : α) → ↥(A (fι a))<VAR>l : List α<GOAL>↑(l.dProd fι fA) = (List.map (fun a => ↑(fA a)) l).prod
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>ι : Sort u_5<VAR>inst✝ : Nonempty ι<VAR>S : ι → Subgroup G<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : G<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f : ι → α<VAR>s✝ t : Set α<VAR>s : Set (α ⊕ β)<GOAL>Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>x : L<GOAL>x ∈ ↑(lieSpan R L s) ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<VAR>s : Set L<VAR>x : L<GOAL>x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → x ∈ K
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : DivisionSemiring α<VAR>inst✝¹ : DivisionSemiring β<VAR>inst✝ : RingHomClass F α β<VAR>f : F<VAR>q : ℚ≥0<GOAL>f ↑q = ↑q
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i j : ι<VAR>h : i ≤ j<VAR>x : G i<GOAL>(s.ι.app j) ((f i j h) x) = (s.ι.app i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i j : ι<VAR>h : i ≤ j<VAR>x : G i<GOAL>(s.ι.app j) ((f i j h) x) = ((directLimitDiagram G f).map (homOfLE h) ≫ s.ι.app j) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i : ι<GOAL>(directLimitCocone G f).ι.app i ≫ (fun s => DirectLimit.lift R ι G f s.ι.app ⋯) s = s.ι.app i
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i : ι<GOAL>∀ (x : ↑((directLimitDiagram G f).obj i)), ((directLimitCocone G f).ι.app i ≫ (fun s => DirectLimit.lift R ι G f s.ι.app ⋯) s) x = (s.ι.app i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i : ι<VAR>x : ↑((directLimitDiagram G f).obj i)<GOAL>(DirectLimit.lift R ι G f s.ι.app ⋯ ∘ₗ DirectLimit.of R ι G f i) x = (s.ι.app i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>i : ι<VAR>x : ↑((directLimitDiagram G f).obj i)<GOAL>(DirectLimit.lift R ι G f s.ι.app ⋯) ((DirectLimit.of R ι G f i) x) = (s.ι.app i) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>m : (directLimitCocone G f).pt ⟶ s.pt<VAR>h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s => DirectLimit.lift R ι G f s.ι.app ⋯) s
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>m : (directLimitCocone G f).pt ⟶ s.pt<VAR>h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j<VAR>this : s.ι.app = fun i => m ∘ₗ DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i<GOAL>m = (fun s => DirectLimit.lift R ι G f s.ι.app ⋯) s
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>m : (directLimitCocone G f).pt ⟶ s.pt<VAR>h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j<VAR>this : s.ι.app = fun i => m ∘ₗ DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i<GOAL>∀ (x : ↑(directLimitCocone G f).pt), m x = ((fun s => DirectLimit.lift R ι G f s.ι.app ⋯) s) x
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>J : Type v<VAR>inst✝⁶ : Category.{t, v} J<VAR>F : J ⥤ ModuleCat R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>inst✝⁵ : Preorder ι<VAR>G : ι → Type v<VAR>inst✝⁴ : (i : ι) → AddCommGroup (G i)<VAR>inst✝³ : (i : ι) → Module R (G i)<VAR>f : (i j : ι) → i ≤ j → G i →ₗ[R] G j<VAR>inst✝² : DirectedSystem G fun i j h => ⇑(f i j h)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>s : Cocone (directLimitDiagram G f)<VAR>m : (directLimitCocone G f).pt ⟶ s.pt<VAR>h : ∀ (j : ι), (directLimitCocone G f).ι.app j ≫ m = s.ι.app j<VAR>this : s.ι.app = fun i => m ∘ₗ DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i<VAR>x : ↑(directLimitCocone G f).pt<GOAL>m x = (DirectLimit.lift R ι G f (fun i => m ∘ₗ DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i) ⋯) x
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>Continuous fun x => (thickenedIndicatorAux δ E x).toNNReal
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>∀ (x : α), thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x : α<GOAL>thickenedIndicatorAux δ E x ∈ {a | a ≠ ⊤}
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>∃ C, ∀ (x y : α), dist ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y) ≤ C
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<GOAL>∀ (x y : α), dist ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y) ≤ 2
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x y : α<GOAL>dist ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) ({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y) ≤ 2
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x y : α<GOAL>|↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) - ↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y)| ≤ 2
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x y : α<GOAL>|↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x)| + |↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y)| ≤ 2
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x y : α<GOAL>↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) + ↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y) ≤ 1 + 1
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>E : Set α<VAR>x y : α<VAR>key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1<GOAL>↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun x) + ↑({ toFun := fun x => (thickenedIndicatorAux δ E x).toNNReal, continuous_toFun := ⋯ }.toFun y) ≤ 1 + 1
<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>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero α<VAR>inst✝ : T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : support f ⊆ k<VAR>h'f : Continuous f<GOAL>f = 0 ∨ LocallyCompactSpace G
<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>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero α<VAR>inst✝ : T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : support f ⊆ k<VAR>h'f : Continuous f<VAR>h : ¬f = 0<GOAL>LocallyCompactSpace G
<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>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero α<VAR>inst✝ : T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : support f ⊆ k<VAR>h'f : Continuous f<VAR>h : ¬∀ (a : G), f a = 0<GOAL>LocallyCompactSpace G
<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>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero α<VAR>inst✝ : T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : support f ⊆ k<VAR>h'f : Continuous f<VAR>x : G<VAR>hx : f x ≠ 0<GOAL>LocallyCompactSpace G
<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>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Zero α<VAR>inst✝ : T1Space α<VAR>f : G → α<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hf : support f ⊆ k<VAR>h'f : Continuous f<VAR>x : G<VAR>hx : f x ≠ 0<VAR>this : k ∈ 𝓝 x<GOAL>LocallyCompactSpace G
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<GOAL>lift.{v', v} (Module.rank R S) ≤ lift.{v, v'} (Module.rank R' S')
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<VAR>this : ((algebraMap R' S').comp i) r = (j.comp (algebraMap R S)) r<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>R✝ : Type u<VAR>R'✝ : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝¹⁵ : Ring R✝<VAR>inst✝¹⁴ : Ring R'✝<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup M'<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R✝ M<VAR>inst✝⁹ : Module R✝ M'<VAR>inst✝⁸ : Module R✝ M₁<VAR>inst✝⁷ : Module R'✝ M'<VAR>inst✝⁶ : Module R'✝ M₁<VAR>R : Type w<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Ring S<VAR>inst✝³ : Algebra R S<VAR>R' : Type w'<VAR>S' : Type v'<VAR>inst✝² : CommRing R'<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra R' S'<VAR>i : R →+* R'<VAR>j : S →+* S'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)<VAR>r : R<VAR>x✝ : S<VAR>this : (algebraMap R' S') (i r) = j ((algebraMap R S) r)<GOAL>↑j (r • x✝) = ↑i r • ↑j x✝
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set 𝕜<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>φ = ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set 𝕜<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>⊤ ≤ StarAlgHom.equalizer φ ψ
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : Algebra 𝕜 A<VAR>inst✝² : TopologicalSpace A<VAR>inst✝¹ : T2Space A<VAR>s : Set 𝕜<VAR>inst✝ : CompactSpace ↑s<VAR>φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)<GOAL>(polynomialFunctions s).starClosure.topologicalClosure ≤ StarAlgHom.equalizer φ ψ
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>Indep (⨆ a, ⨆ n ∈ ns a, s n) (limsup s f) κ μα
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>∀ (i : α), Indep (⨆ n ∈ ns i, s n) (limsup s f) κ μα
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>∀ (i : α), ⨆ n ∈ ns i, s n ≤ m0
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>limsup s f ≤ m0
<VAR>α✝ : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α✝<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α✝ Ω<VAR>μα : Measure α✝<VAR>μ : Measure Ω<VAR>inst✝¹ : IsMarkovKernel κ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>α : Type u_4<VAR>p : Set ι → Prop<VAR>f : Filter ι<VAR>ns : α → Set ι<VAR>h_le : ∀ (n : ι), s n ≤ m0<VAR>h_indep : iIndep s κ μα<VAR>hf : ∀ (t : Set ι), p t → tᶜ ∈ f<VAR>hns : Directed (fun x x_1 => x ≤ x_1) ns<VAR>hnsp : ∀ (a : α), p (ns a)<GOAL>Directed (fun x x_1 => x ≤ x_1) fun i => ⨆ n ∈ ns i, s n
<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>f f₁ g₁ : α₁ → β₁ → Finset γ₁<VAR>g f₂ g₂ : α₂ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<GOAL>(sumLift₂ f g a b).Nonempty ↔ (∃ a₁ b₁, a = inl a₁ ∧ b = inl b₁ ∧ (f a₁ b₁).Nonempty) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ (g a₂ b₂).Nonempty
<VAR>n d a : Int<VAR>a0 : a ≠ 0<GOAL>a * n /. (a * d) = n /. d
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>Q : Type v<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>inj : CategoryTheory.Injective (ModuleCat.of R Q)<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>f : X →ₗ[R] Y<VAR>hf : Function.Injective ⇑f<VAR>g : X →ₗ[R] Q<GOAL>∃ h, ∀ (x : X), h (f x) = g x