ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>p q : ℚ≥0<VAR>n : ℕ<GOAL>↑n = ↑↑n
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : b.fst ≠ x.fst<GOAL>x ∉ sigmaLift f a b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>γ : ι → Type u_4<VAR>inst✝ : DecidableEq ι<VAR>f : ⦃i : ι⦄ → α i → β i → Finset (γ i)<VAR>a : Sigma α<VAR>b : Sigma β<VAR>x : Sigma γ<VAR>h : b.fst ≠ x.fst<GOAL>¬∃ (ha : a.fst = x.fst) (hb : b.fst = x.fst), x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
<VAR>n : ℕ<GOAL>¬BddAbove {p | Prime p}
<VAR>n : ℕ<GOAL>∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y
<VAR>n✝ n : ℕ<GOAL>∃ y ∈ {p | Prime p}, n < y
<VAR>n✝ n p : ℕ<VAR>hi : n.succ ≤ p<VAR>hp : Prime p<GOAL>∃ y ∈ {p | Prime p}, n < y
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Spec : Set (Ideal R) := {I | I.IsPrime}<VAR>s : Finset ↑Spec<VAR>H : ∀ I ∈ range fun x => x.inf Subtype.val, ¬I < (fun x => x.inf Subtype.val) s<GOAL>Spec.Finite
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Spec : Set (Ideal R) := {I | I.IsPrime}<VAR>s : Finset ↑Spec<VAR>H : ∀ I ∈ range fun x => x.inf Subtype.val, ¬I < (fun x => x.inf Subtype.val) s<VAR>p : ↑Spec<GOAL>p ∈ s
<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>f : α → β<VAR>a : α<VAR>h : a ∈ s<GOAL>f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<GOAL>∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>a : ↥circle := ⟨f 1, ⋯⟩<GOAL>∃ a, f = rotation a ∨ f = conjLIE.trans (rotation a)
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>a : ↥circle := ⟨f 1, ⋯⟩<GOAL>f = rotation a ∨ f = conjLIE.trans (rotation a)
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>a : ↥circle := ⟨f 1, ⋯⟩<VAR>this : (f.trans (rotation a).symm) 1 = 1<GOAL>f = rotation a ∨ f = conjLIE.trans (rotation a)
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>a : ↥circle := ⟨f 1, ⋯⟩<VAR>this : (f.trans (rotation a).symm) 1 = 1<VAR>h₁ : f.trans (rotation a).symm = LinearIsometryEquiv.refl ℝ ℂ<GOAL>f = rotation a
<VAR>f : ℂ ≃ₗᵢ[ℝ] ℂ<VAR>a : ↥circle := ⟨f 1, ⋯⟩<VAR>this : (f.trans (rotation a).symm) 1 = 1<VAR>h₂ : f.trans (rotation a).symm = conjLIE<GOAL>f = conjLIE.trans (rotation a)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<GOAL>↑f (1, g) = ↑f (1, 1)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(twoCocycles A)<VAR>g : G<VAR>this : (A.ρ 1) (↑f (1, g)) + ↑f (1, 1 * g) = ↑f (1 * 1, g) + ↑f (1, 1)<GOAL>↑f (1, g) = ↑f (1, 1)
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<GOAL>#↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<VAR>H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n<GOAL>#↑t ≤ ↑n
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<VAR>H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n<VAR>s : Finset ↑t<GOAL>s.card ≤ n
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<VAR>H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n<VAR>s : Finset ↑t<VAR>u : Finset α := Finset.image Subtype.val s<GOAL>s.card ≤ n
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<VAR>H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n<VAR>s : Finset ↑t<VAR>u : Finset α := Finset.image Subtype.val s<VAR>this : u.card = s.card<GOAL>s.card ≤ n
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.216946}<VAR>α : Type u<VAR>n : ℕ<VAR>t : Set α<VAR>H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n<VAR>s : Finset ↑t<VAR>u : Finset α := Finset.image Subtype.val s<VAR>this : u.card = s.card<GOAL>↑u ⊆ t
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y) ^ p = x ^ p - y ^ p
<VAR>R : Type u_1<VAR>inst✝² : Ring R<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP R p<VAR>x y : R<VAR>h : Commute x y<GOAL>(x - y + y) ^ p = x ^ p
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' closedBall b r = closedBall (b / a) r
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁵ : PseudoMetricSpace X<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MulAction G X<VAR>inst✝² : IsometricSMul G X<VAR>inst✝¹ : PseudoMetricSpace G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<VAR>r : ℝ<GOAL>(fun x => x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : FiniteDimensional K V₁<GOAL>Injective ⇑B.flip ↔ Surjective ⇑B
<VAR>K : Type uK<VAR>inst✝⁵ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝⁴ : AddCommGroup V₁<VAR>inst✝³ : Module K V₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>B : V₁ →ₗ[K] V₂ →ₗ[K] K<VAR>inst✝ : FiniteDimensional K V₁<GOAL>Surjective (⇑B.flip.dualMap ∘ ⇑(evalEquiv K V₁).toEquiv) ↔ Surjective ⇑B
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this : PreservesLimitsOfSize.{?u.108151, ?u.108150, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<GOAL>H.IsVanKampen
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝¹ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<VAR>this : ⋯.IsVanKampen<GOAL>H.IsVanKampen
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝¹ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<VAR>this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)<GOAL>IsVanKampenColimit (PushoutCocone.mk h i ⋯)
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝¹ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<VAR>this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)<GOAL>IsVanKampenColimit ((Cocones.precompose (isoWhiskerLeft (span f g) (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj (PushoutCocone.mk h i ⋯))
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝¹ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<VAR>this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)<GOAL>IsColimit (Gl.mapCocone ((Cocones.precompose (spanCompIso Gr f g).hom).obj (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)))
<VAR>J : Type v'<VAR>inst✝¹⁰ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁹ : Category.{v, u} C<VAR>W✝ X✝ Y✝ Z✝ : C<VAR>f✝ : W✝ ⟶ X✝<VAR>g✝ : W✝ ⟶ Y✝<VAR>h✝ : X✝ ⟶ Z✝<VAR>i✝ : Y✝ ⟶ Z✝<VAR>D : Type u''<VAR>inst✝⁸ : Category.{v'', u''} D<VAR>inst✝⁷ : HasPullbacks D<VAR>inst✝⁶ : Adhesive C<VAR>inst✝⁵ : HasPullbacks C<VAR>inst✝⁴ : HasPushouts C<VAR>H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl<VAR>this✝¹ : PreservesColimitsOfSize.{?u.108100, ?u.108099, v, v'', u, u''} Gl<VAR>this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} Gr<VAR>W X Y Z : D<VAR>f : W ⟶ X<VAR>g : W ⟶ Y<VAR>h : X ⟶ Z<VAR>i : Y ⟶ Z<VAR>inst✝ : Mono f<VAR>H : IsPushout f g h i<VAR>this : IsVanKampenColimit (PushoutCocone.mk (pushout.inl (Gr.map f) (Gr.map g)) (pushout.inr (Gr.map f) (Gr.map g)) ⋯)<GOAL>IsColimit ((Cocones.precompose (isoWhiskerLeft (span f g) (asIso adj.counit) ≪≫ (span f g).rightUnitor).hom).obj (PushoutCocone.mk h i ⋯))
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<GOAL>⅟2 • ((mul R R).compl₁₂ LinearMap.id LinearMap.id + (mul R R).compl₁₂ LinearMap.id LinearMap.id) = mul R R
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommSemiring S<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Algebra S R<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<GOAL>(mul R R).compl₁₂ LinearMap.id LinearMap.id = mul R R
<VAR>x y : ℂ<VAR>n : ℕ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n✝ : ℕ<GOAL>(PowerSeries.coeff R n✝) (powerSeriesPart 0) = (PowerSeries.coeff R n✝) 0
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Set G<VAR>hU : ∀ (i : ℕ), IsOpen (U i)<GOAL>μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>U : ℕ → Set G<VAR>hU : ∀ (i : ℕ), IsOpen (U i)<VAR>this : μ.innerContent (⨆ i, { carrier := U i, is_open' := ⋯ }) ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }<GOAL>μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
<VAR>α : Type u<VAR>β : Type v<VAR>γ✝ : Type w<VAR>ι : Sort x<VAR>γ : Type u_1<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : BddBelow (range f)<VAR>hg : Monotone g<GOAL>BddBelow (range (g ∘ f))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : Group α<VAR>inst✝¹ : AddMonoid β<VAR>inst✝ : DistribMulAction α β<VAR>a : α<VAR>x : β<VAR>h : a • x = 0<GOAL>x = 0
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<VAR>hpd2 : p ∣ m * n / p ^ (k + l)<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<VAR>hpd2 : p ∣ m * n / p ^ (k + l)<VAR>hpd3 : p ∣ m * n / (p ^ k * p ^ l)<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<VAR>hpd2 : p ∣ m * n / p ^ (k + l)<VAR>hpd3 : p ∣ m * n / (p ^ k * p ^ l)<VAR>hpd4 : p ∣ m / p ^ k * (n / p ^ l)<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<VAR>hpd2 : p ∣ m * n / p ^ (k + l)<VAR>hpd3 : p ∣ m * n / (p ^ k * p ^ l)<VAR>hpd4 : p ∣ m / p ^ k * (n / p ^ l)<VAR>hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l<GOAL>p ^ (k + 1) ∣ m ∨ p ^ (l + 1) ∣ n
<VAR>n✝ p : ℕ<VAR>p_prime : Prime p<VAR>m n k l : ℕ<VAR>hpm : p ^ k ∣ m<VAR>hpn : p ^ l ∣ n<VAR>hpmn : p ^ (k + l + 1) ∣ m * n<VAR>hpd : p ^ (k + l) * p ∣ m * n<VAR>hpd2 : p ∣ m * n / p ^ (k + l)<VAR>hpd3 : p ∣ m * n / (p ^ k * p ^ l)<VAR>hpd4 : p ∣ m / p ^ k * (n / p ^ l)<VAR>hpd5 : p ∣ m / p ^ k ∨ p ∣ n / p ^ l<GOAL>p ^ k * p ∣ m ∨ p ^ l * p ∣ n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.2047, u_1} D<VAR>W W' : MorphismProperty C<VAR>h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f<GOAL>W = W'
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.2047, u_1} D<VAR>W W' : MorphismProperty C<VAR>h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>W f = W' f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<GOAL>L.map φ.s ≫ φ.map L hL = L.map φ.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<VAR>this : IsIso (L.map φ.s) := hL φ.s φ.hs<GOAL>L.map φ.s ≫ φ.map L hL = L.map φ.f
<VAR>x✝ y x : ℝ<VAR>hx : 1 ≤ x<GOAL>arcsin x = π / 2
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>x : G<VAR>hx : x ∈ center G<VAR>y : G<GOAL>y ∈ H ↔ x * y * x⁻¹ ∈ H
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<GOAL>HasPDF (g ∘ X) ℙ ν
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<GOAL>AEMeasurable (g ∘ X) ℙ ∧ (map g (map X ℙ)).HaveLebesgueDecomposition ν ∧ map g (map X ℙ) ≪ ν
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<GOAL>map g (map X ℙ) ≪ ν
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<GOAL>map g (μ.withDensity (pdf X ℙ μ)) ≪ ν
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<VAR>s : Set F<VAR>hsm : MeasurableSet s<VAR>hs : ν s = 0<GOAL>(map g (μ.withDensity (pdf X ℙ μ))) s = 0
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<VAR>s : Set F<VAR>hsm : MeasurableSet s<VAR>hs : ν s = 0<GOAL>∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ μ a ∂μ = 0
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<VAR>s : Set F<VAR>hsm : MeasurableSet s<VAR>hs : ν s = 0<VAR>this : (map g μ) s = 0<GOAL>∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ μ a ∂μ = 0
<VAR>Ω✝ : Type u_1<VAR>E✝ : Type u_2<VAR>inst✝⁴ : MeasurableSpace E✝<VAR>m✝ : MeasurableSpace Ω✝<VAR>ℙ✝ : Measure Ω✝<VAR>μ✝ : Measure E✝<VAR>F✝ : Type u_3<VAR>inst✝³ : MeasurableSpace F✝<VAR>ν✝ : Measure F✝<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝² : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>F : Type u_3<VAR>inst✝¹ : MeasurableSpace F<VAR>ν : Measure F<VAR>X : Ω → E<VAR>inst✝ : HasPDF X ℙ μ<VAR>hX : AEMeasurable X ℙ<VAR>g : E → F<VAR>hg : QuasiMeasurePreserving g μ ν<VAR>hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν<VAR>hmX : Measurable X<VAR>s : Set F<VAR>hsm : MeasurableSet s<VAR>hs : ν s = 0<VAR>this : μ (g ⁻¹' s) = 0<GOAL>∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ μ a ∂μ = 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hq : q ≠ 0<GOAL>q / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hq : q ≠ 0<VAR>r : R<VAR>hr : q = GCDMonoid.gcd p q * r<GOAL>q / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hq : q ≠ 0<VAR>r : R<VAR>hr : q = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>q / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hq : q ≠ 0<VAR>r : R<VAR>hr : q = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>GCDMonoid.gcd p q * r / GCDMonoid.gcd p q ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : GCDMonoid R<VAR>p✝ q✝ p q : R<VAR>hq : q ≠ 0<VAR>r : R<VAR>hr : q = GCDMonoid.gcd p q * r<VAR>pq0 : GCDMonoid.gcd p q ≠ 0<VAR>r0 : r ≠ 0<GOAL>r ≠ 0
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (StructuredArrow d F)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(F.map f.unop.right).op ≫ (unop Y✝).hom.op = (unop X✝).hom.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>d : D<VAR>X✝ Y✝ : (StructuredArrow d F)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<GOAL>(𝟙 d ≫ (unop X✝).hom).op = (unop X✝).hom.op
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Chain R a l<VAR>hb : b ∈ l<GOAL>R a b
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁ l₂ : List α<VAR>a b : α<VAR>inst✝ : IsTrans α R<VAR>hl : Pairwise R (a :: l)<VAR>hb : b ∈ l<GOAL>R a b
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>A : W ≃ₗᵢ[ℝ] V<VAR>f : V → E<VAR>w : W<GOAL>𝓕 (f ∘ ⇑A) w = 𝓕 f (A w)