ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 / 2)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>{p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable ↔ ∃ x, x ∈ {p | S ⊆ ↑p}
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>(∃ x, x ∈ {p | S ⊆ ↑p}) → ((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<VAR>p : T.CompleteType α<VAR>hp : p ∈ {p | S ⊆ ↑p}<GOAL>((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : AddCommGroup M''<VAR>inst✝ : Module R M''<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>r : R<VAR>a✝ : IsSMulRegular (M ⧸ N) r<GOAL>r • ⊤ ⊓ N = map (DistribMulAction.toLinearMap R M r) (comap ((LinearMap.lsmul R M) r) N)
<VAR>z : ℂ<GOAL>|z.re| ≤ abs z
<VAR>z : ℂ<GOAL>z.re * z.re ≤ normSq z
<VAR>n m : ℕ<VAR>j : Fin n<VAR>i : Fin (n + 1)<VAR>hi : i ≠ 0<GOAL>j < i.pred hi ↔ j.succ < i
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B✝ C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : Nontrivial 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<GOAL>∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : Nontrivial 𝕜<VAR>A : Set E<VAR>hAB : IsExposed 𝕜 A ∅<GOAL>∃ l a, ∅ = {x | x ∈ A ∧ a ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace 𝕜<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : Module 𝕜 E<VAR>l : E →L[𝕜] 𝕜<VAR>A✝ B✝ C : Set E<VAR>X : Finset E<VAR>x : E<VAR>inst✝ : Nontrivial 𝕜<VAR>A B : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>hB : B.Nonempty<GOAL>∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c d a b : G<GOAL>a / (a * b) = b⁻¹
<VAR>k : Type u<VAR>inst✝¹ : Field k<VAR>G : Type u<VAR>inst✝ : Group G<VAR>V W : FDRep k G<VAR>g : G<GOAL>(of (linHom V.ρ W.ρ)).character g = V.character g⁻¹ * W.character g
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>inst✝ : DecidableEq α<VAR>h : a ∈ s<GOAL>a * (s.erase a).prod = s.prod
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>inst✝ : DecidableEq ι<VAR>i✝ i : ι<VAR>h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y<VAR>ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)<GOAL>∀ (a : α i), Acc (DFinsupp.Lex r s) (single i a)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>inst✝ : DecidableEq ι<VAR>i✝ i : ι<VAR>h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y<VAR>ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)<VAR>a✝ a : α i<VAR>ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y<GOAL>(fun x => Acc (DFinsupp.Lex r s) (single i x)) a
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs✝ : ∀ (i : ι), WellFounded (s i)<VAR>inst✝ : DecidableEq ι<VAR>i✝ i : ι<VAR>h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y<VAR>ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)<VAR>a✝ a : α i<VAR>ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y<VAR>x : Π₀ (i : ι), α i<VAR>k : ι<VAR>hr : ∀ (j : ι), r j k → x j = (single i a) j<VAR>hs : s k (x k) ((single i a) k)<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Zero (α i)<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0<VAR>hs✝ : ∀ (i : ι), WellFounded (s i)<VAR>inst✝ : DecidableEq ι<VAR>i✝ i : ι<VAR>h✝ : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → Acc (rᶜ ⊓ fun x x_1 => x ≠ x_1) y<VAR>ih : ∀ (y : ι), (rᶜ ⊓ fun x x_1 => x ≠ x_1) y i → ∀ (a : α y), Acc (DFinsupp.Lex r s) (single y a)<VAR>a✝ a : α i<VAR>ha : ∀ (y : α i), s i y a → (fun x => Acc (DFinsupp.Lex r s) (single i x)) y<VAR>x : Π₀ (i : ι), α i<VAR>k : ι<VAR>hr : ∀ (j : ι), r j k → x j = (single i a) j<VAR>hs : s k (x k) (if h : i = k then Eq.recOn h a else 0)<GOAL>Acc (DFinsupp.Lex r s) x
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>hb : b ≠ 0<VAR>h : a * b = c<GOAL>a = c / b
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set V<GOAL>G'.deleteVerts s ≤ G'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<GOAL>U R (-↑(k + 1) + 2) = 2 * X * U R (-↑(k + 1) + 1) - U R (-↑(k + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : Measure α<GOAL>(mapₗ f) μ = map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f : α → β<VAR>hf : Measurable f<VAR>μ : Measure α<GOAL>(mapₗ f) μ = (mapₗ (AEMeasurable.mk f ⋯)) μ
<VAR>m k n : ℕ+<GOAL>m ∣ k → k.Coprime n → m.Coprime n
<VAR>m k n : ℕ+<GOAL>↑m ∣ ↑k → k.Coprime n → m.Coprime n
<VAR>m k n : ℕ+<GOAL>↑m ∣ ↑k → (↑k).Coprime ↑n → (↑m).Coprime ↑n
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>u : αˣ<VAR>hu : ↑u = a<GOAL>IsUnit a⁻¹
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>u : αˣ<VAR>hu : ↑u = a<GOAL>IsUnit ↑u⁻¹
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>m : Multiset α<VAR>a : α<VAR>ha : a ∈ m<GOAL>a ≤ m.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a : α<VAR>t : Multiset α<VAR>ha : a ∈ a ::ₘ t<GOAL>a ≤ (a ::ₘ t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a : α<VAR>t : Multiset α<VAR>ha : a ∈ a ::ₘ t<GOAL>a ≤ a * t.prod
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<GOAL>x = e.orientation ∨ x = -e.orientation
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx : x ≠ 0<GOAL>rayOfNeZero R x hx = e.orientation ∨ rayOfNeZero R x hx = -e.orientation
<VAR>R : Type u_1<VAR>inst✝⁴ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι : Type u_3<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>e : Basis ι R M<VAR>x : M [⋀^ι]→ₗ[R] R<VAR>hx✝ : x ≠ 0<VAR>hx : x ⇑e ≠ 0<GOAL>rayOfNeZero R x hx✝ = e.orientation ∨ rayOfNeZero R x hx✝ = -e.orientation
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : DecidableEq G<VAR>R S : Finset G<VAR>hR : ↑R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure ↑S = ⊤<GOAL>closure ↑(Finset.image (fun g => ⟨g * (↑(toFun hR g))⁻¹, ⋯⟩) (R * S)) = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : DecidableEq G<VAR>R S : Finset G<VAR>hR : ↑R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<VAR>hS : closure ↑S = ⊤<GOAL>closure ((fun g => ⟨g * (↑(toFun hR g))⁻¹, ⋯⟩) '' (↑R * ↑S)) = ⊤
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>inst✝ : (i : ι) → SMul K (R i)<VAR>r : K<VAR>t : (i : ι) → Set (R i)<VAR>x : (i : ι) → R i<VAR>h : x ∈ univ.pi (r • t)<GOAL>x ∈ r • univ.pi t
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>inst✝ : (i : ι) → SMul K (R i)<VAR>r : K<VAR>t : (i : ι) → Set (R i)<VAR>x : (i : ι) → R i<VAR>h : x ∈ univ.pi (r • t)<VAR>i : ι<VAR>x✝ : i ∈ univ<GOAL>(fun i => Classical.choose ⋯) i ∈ t i
<VAR>K : Type u_1<VAR>ι : Type u_2<VAR>R : ι → Type u_3<VAR>inst✝ : (i : ι) → SMul K (R i)<VAR>r : K<VAR>t : (i : ι) → Set (R i)<VAR>x : (i : ι) → R i<VAR>h : x ∈ univ.pi (r • t)<VAR>i : ι<GOAL>(fun x => r • x) (fun i => Classical.choose ⋯) i = x i
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b a : α<VAR>f : ι → α<GOAL>a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>Irreducible p ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>(∀ (q : R[X]), q.degree ≤ ↑((p * C p.leadingCoeff⁻¹).natDegree / 2) → q ∣ p * C p.leadingCoeff⁻¹ → IsUnit q) ↔ ∀ (q : R[X]), q.degree ≤ ↑(p.natDegree / 2) → q ∣ p → IsUnit q
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Field R<VAR>p✝ q p : R[X]<VAR>hp0 : p ≠ 0<VAR>hpu : ¬IsUnit p<GOAL>p * C p.leadingCoeff⁻¹ ≠ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖x‖ = C * integral μ (map norm f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace ℝ F'<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : SMulCommClass ℝ 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖x‖ = C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal • ‖x‖
<VAR>α : Type u<VAR>β : α → Type v<VAR>l✝ l₁ l₂ : List (Sigma β)<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>dlookup a l = none ↔ a ∉ l.keys
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>h : MeasurePreserving (⇑e) μ μ'<GOAL>Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>h : MeasurePreserving (⇑e) μ μ'<VAR>this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ<GOAL>Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>β : Type u_2<VAR>m' : MeasurableSpace β<VAR>μ' : Measure β<VAR>s' : Set β<VAR>g : α → β<VAR>e : α ≃ᵐ β<VAR>this : MeasurePreserving (⇑e ∘ f ∘ ⇑e.symm) μ' μ' ↔ MeasurePreserving f μ μ<VAR>h : PreErgodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ PreErgodic f μ<GOAL>Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>hXY : M.closure X ⊂ M.closure Y<GOAL>∃ e ∈ Y, e ∉ M.closure X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>hXY : M.closure X ⊂ M.closure Y<VAR>hcon : ∀ e ∈ Y, e ∈ M.closure X<GOAL>False
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>(1 + z).arg ∈ Set.Ioo (-(π / 2)) (π / 2)
<VAR>z : ℂ<VAR>hz : ‖z‖ < 1<GOAL>-1 < z.re ∨ 1 + z = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : TopologicalSpace E<VAR>p : SeminormFamily 𝕜 E ι<VAR>hp : WithSeminorms p<VAR>u : F → E<VAR>f : Filter F<VAR>y₀ : E<GOAL>Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>((const α c).restrict s).lintegral μ = c * μ s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Monoid G<VAR>a : G<VAR>n : ℕ<VAR>inst✝ : MulAction G H<VAR>b : H<GOAL>(fun x => a • x)^[n] b = a ^ n • b
<VAR>x y : ℂ<GOAL>cos x ^ 2 = 1 / 2 + cos (2 * x) / 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h : W.Nonsingular (u • P)<GOAL>W.Nonsingular P
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h✝ : W.Nonsingular (u • P)<VAR>h : W.Equation (u • P)<VAR>h' : W.a₁ * (u • P) 1 * (u • P) 2 ≠ 3 * (u • P) 0 ^ 2 + 2 * W.a₂ * (u • P) 0 * (u • P) 2 + W.a₄ * (u • P) 2 ^ 2 ∨ (u • P) 1 * (u • P) 2 ≠ -(u • P) 1 * (u • P) 2 - W.a₁ * (u • P) 0 * (u • P) 2 - W.a₃ * (u • P) 2 ^ 2 ∨ (u • P) 1 ^ 2 + W.a₁ * (u • P) 0 * (u • P) 1 + 2 * W.a₃ * (u • P) 1 * (u • P) 2 ≠ W.a₂ * (u • P) 0 ^ 2 + 2 * W.a₄ * (u • P) 0 * (u • P) 2 + 3 * W.a₆ * (u • P) 2 ^ 2<GOAL>W.Nonsingular P
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h✝ : W.Nonsingular (u • P)<VAR>h : W.Equation (u • P)<VAR>h' : W.a₁ * (u • P) 1 * (u • P) 2 ≠ 3 * (u • P) 0 ^ 2 + 2 * W.a₂ * (u • P) 0 * (u • P) 2 + W.a₄ * (u • P) 2 ^ 2 ∨ (u • P) 1 * (u • P) 2 ≠ -(u • P) 1 * (u • P) 2 - W.a₁ * (u • P) 0 * (u • P) 2 - W.a₃ * (u • P) 2 ^ 2 ∨ (u • P) 1 ^ 2 + W.a₁ * (u • P) 0 * (u • P) 1 + 2 * W.a₃ * (u • P) 1 * (u • P) 2 ≠ W.a₂ * (u • P) 0 ^ 2 + 2 * W.a₄ * (u • P) 0 * (u • P) 2 + 3 * W.a₆ * (u • P) 2 ^ 2<GOAL>W.a₁ * P 1 * P 2 ≠ 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∨ P 1 * P 2 ≠ -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 ∨ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 ≠ W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h✝ : W.Nonsingular (u • P)<VAR>h : W.Equation (u • P)<VAR>h' : W.a₁ * P 1 * P 2 = 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∧ P 1 * P 2 = -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 ∧ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 = W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2<GOAL>W.a₁ * (u • P) 1 * (u • P) 2 = 3 * (u • P) 0 ^ 2 + 2 * W.a₂ * (u • P) 0 * (u • P) 2 + W.a₄ * (u • P) 2 ^ 2 ∧ (u • P) 1 * (u • P) 2 = -(u • P) 1 * (u • P) 2 - W.a₁ * (u • P) 0 * (u • P) 2 - W.a₃ * (u • P) 2 ^ 2 ∧ (u • P) 1 ^ 2 + W.a₁ * (u • P) 0 * (u • P) 1 + 2 * W.a₃ * (u • P) 1 * (u • P) 2 = W.a₂ * (u • P) 0 ^ 2 + 2 * W.a₄ * (u • P) 0 * (u • P) 2 + 3 * W.a₆ * (u • P) 2 ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P✝ : Fin 3 → R<VAR>u✝ u : Rˣ<VAR>P : Fin 3 → R<VAR>h✝ : W.Nonsingular (u • P)<VAR>h : W.Equation (u • P)<VAR>h' : W.a₁ * P 1 * P 2 = 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 ∧ P 1 * P 2 = -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 ∧ P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 = W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2<GOAL>W.a₁ * (↑u * P 1) * (↑u * P 2) = 3 * (↑u * P 0) ^ 2 + 2 * W.a₂ * (↑u * P 0) * (↑u * P 2) + W.a₄ * (↑u * P 2) ^ 2 ∧ ↑u * P 1 * (↑u * P 2) = -(↑u * P 1) * (↑u * P 2) - W.a₁ * (↑u * P 0) * (↑u * P 2) - W.a₃ * (↑u * P 2) ^ 2 ∧ (↑u * P 1) ^ 2 + W.a₁ * (↑u * P 0) * (↑u * P 1) + 2 * W.a₃ * (↑u * P 1) * (↑u * P 2) = W.a₂ * (↑u * P 0) ^ 2 + 2 * W.a₄ * (↑u * P 0) * (↑u * P 2) + 3 * W.a₆ * (↑u * P 2) ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<VAR>u : Rˣ<VAR>this : ∀ (u : Rˣ) {P : Fin 3 → R}, W.Nonsingular (u • P) → W.Nonsingular P<VAR>h : W.Nonsingular P<GOAL>W.Nonsingular (u⁻¹ • u • P)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < 1 - ε ↑(r i n)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < 1 - ε ↑(r i x)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>f : α → β<VAR>comm : {x | x ∈ s ∪ t}.Pairwise fun a b => Commute (f a) (f b)<GOAL>(s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : DecidableEq α<VAR>t : Finset α<VAR>f : α → β<VAR>sl : List α<VAR>sl' : sl.Nodup<VAR>h : Disjoint sl.toFinset t<VAR>comm : {x | x ∈ sl.toFinset ∪ t}.Pairwise fun a b => Commute (f a) (f b)<GOAL>(sl.toFinset ∪ t).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * t.noncommProd f ⋯
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>sl : List α<VAR>sl' : sl.Nodup<VAR>tl : List α<VAR>tl' : tl.Nodup<VAR>h : Disjoint sl.toFinset tl.toFinset<VAR>comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise fun a b => Commute (f a) (f b)<GOAL>(sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>sl : List α<VAR>sl' : sl.Nodup<VAR>tl : List α<VAR>tl' : tl.Nodup<VAR>h : sl.Disjoint tl<VAR>comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise fun a b => Commute (f a) (f b)<GOAL>(sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>0 < angle x (x - y)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>0 < angle x (x - y)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ -y ≠ 0<GOAL>0 < angle x (x - y)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ -y ≠ 0<GOAL>0 < angle x (x + -y)
<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>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<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>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<VAR>u : ℕ → Set G<VAR>hu : (𝓝 1).HasBasis (fun x => True) u<VAR>u_anti : Antitone u<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<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>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<VAR>u : ℕ → Set G<VAR>hu : (𝓝 1).HasBasis (fun x => True) u<VAR>u_anti : Antitone u<VAR>this : ∀ (ib : ℕ), True → ∃ ia, (True ∧ True) ∧ ∀ x ∈ u ia.1 ×ˢ u ia.2, x.1 * x.2 ∈ u ib<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<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>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<VAR>u : ℕ → Set G<VAR>hu : (𝓝 1).HasBasis (fun x => True) u<VAR>u_anti : Antitone u<VAR>this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n
<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>N : Subgroup G<VAR>n : N.Normal<VAR>inst✝ : FirstCountableTopology G<VAR>u : ℕ → Set G<VAR>hu : (𝓝 1).HasBasis (fun x => True) u<VAR>u_anti : Antitone u<VAR>this : ∀ (ib : ℕ), ∃ a b, True ∧ ∀ (a_1 b_1 : G), a_1 ∈ u a → b_1 ∈ u b → a_1 * b_1 ∈ u ib<VAR>event_mul : ∀ (n : ℕ), ∀ᶠ (m : ℕ) in atTop, u m * u m ⊆ u n<GOAL>∃ u, (𝓝 1).HasAntitoneBasis u ∧ ∀ (n : ℕ), u (n + 1) * u (n + 1) ⊆ u n