ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<VAR>n : ℕ<VAR>hn : n ∈ g'.cycleType<GOAL>n ∣ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<VAR>n : ℕ<VAR>hn : n ∈ g'.cycleType<GOAL>g'.support.card ≤ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<VAR>n : ℕ<VAR>hn : n ∈ g'.cycleType<GOAL>?a + g'.support.card ≤ ?a + 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<VAR>n : ℕ<VAR>hn : n ∈ g'.cycleType<GOAL>ℕ
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>c g' : Perm (Fin 5)<VAR>h : 3 ∈ (c * g').cycleType<VAR>hd : c.Disjoint g'<VAR>left✝ : c.IsCycle<VAR>h3 : c.support.card = 3<VAR>n : ℕ<VAR>hn : n ∈ g'.cycleType<GOAL>(c * g').support.card ≤ 3 + 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a✝ b : α<VAR>s✝ : Finset β<VAR>inst✝ : ContinuousMul α<VAR>f : γ → β → α<VAR>a : γ → α<VAR>s : Finset γ<GOAL>(∀ i ∈ s, HasProd (f i) (a i)) → HasProd (fun b => ∏ i ∈ s, f i b) (∏ i ∈ s, a i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<GOAL>eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>x : α<GOAL>(fun x => ↑‖(f + g) x‖₊) x ≤ ((fun x => ↑‖f x‖₊) + fun x => ↑‖g x‖₊) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>f✝ g✝ f g : α → E<VAR>x : α<GOAL>‖f x + g x‖₊ ≤ ‖f x‖₊ + ‖g x‖₊
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R (m + n)) ((monomial R m) a * φ) = a * (coeff R n) φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>a : R<GOAL>m ≤ m + n
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{?u.37071, u_1} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>epimorphisms C f ↔ Epi f
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>q n : ℕ<VAR>x y : R<VAR>h : Commute x y<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP R q<VAR>this : Fact (Nat.Prime q)<GOAL>(x - y) ^ q ^ n = x ^ q ^ n - y ^ q ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : NoAccidental t<VAR>x✝ : Finset (α ⊕ β ⊕ γ)<GOAL>x✝ ∈ (graph t).cliqueSet 3 ↔ x✝ ∈ ⇑toTriangle '' ↑t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y x : α<VAR>hx : f x ≠ x<VAR>h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<GOAL>(g * f * g⁻¹).IsCycle
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y✝ x : α<VAR>hx : f x ≠ x<VAR>h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>y : α<VAR>hy : (g * f * g⁻¹) y ≠ y<GOAL>(g * f * g⁻¹).SameCycle (g x) y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x✝ y✝ x : α<VAR>hx : f x ≠ x<VAR>h : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y<VAR>y : α<VAR>hy : (g * f * g⁻¹) y ≠ y<GOAL>(g * f * g⁻¹).SameCycle (g x) (g (g⁻¹ y))
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>x ∈ RingHom.ker toZMod ↔ x ∈ maximalIdeal ℤ_[p]
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>r : ℚ<VAR>x✝ x : ℤ_[p]<GOAL>toZMod x = 0 ↔ x ∈ maximalIdeal ℤ_[p]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddCommGroup α<VAR>h : Periodic f c<VAR>a x : α<GOAL>(fun x => f (a - x)) (x + c) = (fun x => f (a - x)) x
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ‖ -x ↔ 0 ‖ x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set Y<VAR>h : X ≃ₜ Y<GOAL>IsPreconnected (⇑h ⁻¹' s) ↔ IsPreconnected s
<VAR>x✝ y x : ℝ<VAR>n : ℕ<GOAL>↑(rexp (↑n * x)) = ↑(rexp x ^ n)
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<GOAL>p.smeval 0 = p.coeff 0 • 1
<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>f : α → β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ filter p s, 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>f : α → β<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>∏ x ∈ map (Embedding.subtype p) (Finset.subtype p s), f x = ∏ x ∈ filter p s, f x
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>μ_fin : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c<GOAL>∫⁻ (x : α), f x ∂μ < ⊤
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>μ_fin : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c<GOAL>∫⁻ (x : α) in univ, f x ∂μ < ⊤
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α✝<VAR>μ✝ ν : Measure α✝<VAR>α : Type u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>μ_fin : IsFiniteMeasure μ<VAR>f : α → ℝ≥0∞<VAR>f_bdd : ∃ c, ∀ (x : α), f x ≤ ↑c<GOAL>∃ y, ∀ x ∈ univ, f x ≤ ↑y
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace B<VAR>inst✝⁵ : TopologicalSpace (TotalSpace F E)<VAR>e✝ : Trivialization F TotalSpace.proj<VAR>x : TotalSpace F E<VAR>b✝ : B<VAR>y : E b✝<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : Module R F<VAR>inst✝² : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹ : (x : B) → Module R (E x)<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : Trivialization.IsLinear R e<VAR>b : B<VAR>hb : b ∈ e.baseSet<GOAL>⇑(Trivialization.linearMapAt R e b) = fun y => (↑e { proj := b, snd := y }).2
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>p.support.Nonempty ↔ p ≠ 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b₁ b₂ : P<GOAL>(s.weightedVSubOfPoint p b₁) w = (s.weightedVSubOfPoint p b₂) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b₁ b₂ : P<GOAL>(s.weightedVSubOfPoint p b₁) w - (s.weightedVSubOfPoint p b₂) w = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b₁ b₂ : P<GOAL>∑ x ∈ s, (w x • (p x -ᵥ b₁) - w x • (p x -ᵥ b₂)) = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>h : ∑ i ∈ s, w i = 0<VAR>b₁ b₂ : P<GOAL>∑ x ∈ s, w x • (b₂ -ᵥ b₁) = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<GOAL>(GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback f ↑S), ⋯⟩).arrows g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<GOAL>s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } ≫ α.app (op W) = s.ι i ≫ R.map h.op ≫ α.app (op W)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<GOAL>s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } ≫ α.app (op W) = (s.ι i ≫ R.map h.op) ≫ α.app (op W)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<GOAL>s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>Y : C<VAR>f : G.obj Y ⟶ X<VAR>W : C<VAR>g : W ⟶ Y<VAR>i : S.Arrow<VAR>h : G.obj W ⟶ i.Y<VAR>w : h ≫ i.f = G.map g ≫ f<VAR>r : S.Relation := { fst := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }, snd := i, r := { Z := { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }.Y, g₁ := 𝟙 { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ }.Y, g₂ := h, w := ⋯ } }<GOAL>s.ι { Y := G.obj W, f := G.map g ≫ f, hf := ⋯ } = s.ι i ≫ R.map h.op
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>hstf : f ≤ 𝓟 (s ∩ t)<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>hstf : f ≤ 𝓟 (s ∩ t)<VAR>x : X<VAR>hsx : x ∈ s<VAR>hx : ClusterPt x f<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsClosed t<VAR>f : Filter X<VAR>hnf : f.NeBot<VAR>hstf : f ≤ 𝓟 (s ∩ t)<VAR>x : X<VAR>hsx : x ∈ s<VAR>hx : ClusterPt x f<VAR>this : x ∈ t<GOAL>∃ x ∈ s ∩ t, ClusterPt x f
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<GOAL>μ (s * closure {1}) = μ s
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<GOAL>μ (s * closure {1}) ≤ μ s
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<GOAL>μ (s * closure {1}) ≤ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<GOAL>∀ (i : Set G), s ⊆ i → MeasurableSet i → μ (s * closure {1}) ≤ μ i
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<VAR>t : Set G<VAR>kt : s ⊆ t<VAR>t_meas : MeasurableSet t<GOAL>μ (s * closure {1}) ≤ μ t
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<VAR>t : Set G<VAR>kt : s ⊆ t<VAR>t_meas : MeasurableSet t<GOAL>s * closure {1} ⊆ t
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ✝ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ✝.IsMulLeftInvariant<VAR>s : Set G<VAR>μ : Measure G<VAR>t : Set G<VAR>kt : s ⊆ t<VAR>t_meas : MeasurableSet t<GOAL>s * closure {1} ⊆ t * closure {1}
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : CharP R p<VAR>h : ↑p = 0<GOAL>False
<VAR>A : Type u_1<VAR>inst✝⁴ : NormedRing A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : A<VAR>ha : IsSelfAdjoint a<GOAL>(spectralRadius ℂ a).toReal = ‖a‖
<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>u : κ → UniformSpace α'<VAR>F : ι → X → α'<GOAL>Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F
<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>u : κ → UniformSpace α'<VAR>F : ι → X → α'<GOAL>Continuous (⇑UniformFun.ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous (⇑UniformFun.ofFun ∘ swap F)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>this✝ : ‖x‖ ≠ 0<VAR>this : ‖y‖ ≠ 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>this✝ : ‖x‖ ≠ 0<VAR>this : ‖y‖ ≠ 0<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>this✝ : ‖x‖ ≠ 0<VAR>this : ‖y‖ ≠ 0<GOAL>(o.kahler x) y ≠ 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₃' : P<VAR>h : Sbtw ℝ p₃ p₂ p₃'<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ↑π
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : NumberField k<VAR>inst✝ : IsGalois k K<GOAL>(filter (IsUnramified k) univ).card = (filter (IsUnramifiedIn K) univ).card * finrank k K
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : NumberField k<VAR>inst✝ : IsGalois k K<VAR>this : Module.Finite k K := Module.Finite.of_restrictScalars_finite ℚ k K<GOAL>(filter (IsUnramified k) univ).card = (filter (IsUnramifiedIn K) univ).card * finrank k K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N✝ : Matroid β<VAR>E B I : Set α<VAR>N : Matroid β<VAR>f : α → β<GOAL>N.comapOn (f ⁻¹' N.E) f = N.comap f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E✝ I✝ s : Set α<VAR>M : Matroid α<VAR>N✝ : Matroid β<VAR>E B I : Set α<VAR>N : Matroid β<VAR>f : α → β<GOAL>f ⁻¹' N.E = (N.comap f).E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_zero : c ≠ 0<GOAL>Continuous fun x => x / c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_zero : c ≠ 0<GOAL>∀ (x : ℝ≥0∞), ContinuousAt (fun x => x * c⁻¹) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>c : ℝ≥0∞<VAR>c_ne_zero : c ≠ 0<VAR>x : ℝ≥0∞<GOAL>ContinuousAt (fun x => x * c⁻¹) x
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>a⁻¹ * a < b * a ↔ 1 < b * a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_2, u_1} C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : Preadditive C<VAR>inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹ : Pretriangulated C<VAR>S : Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>S.W f
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_2, u_1} C<VAR>inst✝⁵ : HasZeroObject C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : Preadditive C<VAR>inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝¹ : Pretriangulated C<VAR>S : Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<GOAL>Arrow.mk (𝟙 X) ≅ Arrow.mk f
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x✝ y : G<VAR>n✝ m : ℕ<VAR>x : G<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>dvd : n ∣ orderOf x<GOAL>orderOf (x ^ n) = orderOf x / n
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : HasUpperLowerClosure α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>(interior s).OrdConnected
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : HasUpperLowerClosure α<VAR>s : Set α<VAR>h : s.OrdConnected<GOAL>(interior ↑(upperClosure s) ∩ interior ↑(lowerClosure s)).OrdConnected
<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>(∃ i, G.moveLeft i ≈ 0) ↔ G ‖ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>hn : G ‖ 0<GOAL>∃ i, G.moveLeft i ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>hn : ∃ i, 0 ≤ G.moveLeft i<GOAL>∃ i, G.moveLeft i ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>i : G.LeftMoves<VAR>hi : 0 ≤ G.moveLeft i<GOAL>∃ i, G.moveLeft i ≈ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>IndepFun X' Y' μ'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>(Measure.map X μ).prod (Measure.map Y μ) = (Measure.map X' μ').prod (Measure.map Y' μ')