ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<VAR>K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }<VAR>S : ℕ → ConvexBody E := fun n => (1 + u n) • K<VAR>Z : ℕ → Set E := fun n => ↑(S n) ∩ (↑L \ {0})<VAR>h_zero : 0 ∈ K<VAR>h_clos : IsClosed (↑L \ {0})<GOAL>(⋂ n, Z n).Nonempty
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<VAR>K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }<VAR>S : ℕ → ConvexBody E := fun n => (1 + u n) • K<VAR>Z : ℕ → Set E := fun n => ↑(S n) ∩ (↑L \ {0})<VAR>h_zero : 0 ∈ K<VAR>h_clos : IsClosed (↑L \ {0})<VAR>n : ℕ<GOAL>Z (n + 1) ⊆ Z n
<VAR>E : Type u_1<VAR>L✝ : Type u_2<VAR>inst✝⁸ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>L : AddSubgroup E<VAR>inst✝¹ : Countable ↥L<VAR>inst✝ : DiscreteTopology ↥L<VAR>fund : IsAddFundamentalDomain (↥L) F μ<VAR>h_symm : ∀ x ∈ s, -x ∈ s<VAR>h_conv : Convex ℝ s<VAR>h_cpt : IsCompact s<VAR>h : μ F * 2 ^ finrank ℝ E ≤ μ s<VAR>h_mes : μ s ≠ 0<VAR>h_nemp : s.Nonempty<VAR>u : ℕ → ℝ≥0 := ⋯.choose<VAR>K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }<VAR>S : ℕ → ConvexBody E := fun n => (1 + u n) • K<VAR>Z : ℕ → Set E := fun n => ↑(S n) ∩ (↑L \ {0})<VAR>h_zero : 0 ∈ K<VAR>h_clos : IsClosed (↑L \ {0})<VAR>n : ℕ<GOAL>(Z n).Nonempty
<VAR>X Y : Scheme<VAR>U✝ : X.Opens<VAR>hU : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X, U✝)<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : { U // ↑U ≤ Scheme.Hom.opensRange f }<GOAL>IsAffineOpen (f ''ᵁ f ⁻¹ᵁ ↑↑U)
<VAR>X Y : Scheme<VAR>U✝ : X.Opens<VAR>hU : IsAffineOpen U✝<VAR>f✝ : ↑Γ(X, U✝)<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : { U // ↑U ≤ Scheme.Hom.opensRange f }<GOAL>IsAffineOpen ↑↑U
<VAR>p q r : Prop<VAR>h : r → p → q<GOAL>r ∧ p → r ∧ q
<VAR>f : ℕ →. ℕ<VAR>hf : Partrec f<GOAL>Partrec₂ fun a m => Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + m)))
<VAR>f : ℕ →. ℕ<VAR>hf : Partrec f<GOAL>Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
<VAR>f : ℕ →. ℕ<VAR>hf : Partrec f<VAR>this : Partrec fun a => Nat.rfind fun n => (fun m => decide (m = 0)) <$> unpaired (fun a b => f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)<GOAL>Partrec (unpaired fun a b => Nat.rfind fun n => (fun m => decide (m = 0)) <$> f (Nat.pair a (n + b)))
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>f g : α ⟹ β<VAR>h : ∀ (i : Fin2 n), f i = g i<GOAL>f = g
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>β : TypeVec.{u_2} n<VAR>f g : α ⟹ β<VAR>h : ∀ (i : Fin2 n), f i = g i<VAR>i : Fin2 n<GOAL>f i = g i
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' Ioo ⊥ ↑y = Iio y
<VAR>y : ℝ<GOAL>Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : DilationClass F α β<VAR>f : F<VAR>x y : α<VAR>key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤<GOAL>edist (f x) (f y) = ↑⋯.choose * edist x y
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>μ : CyclotomicField n K<VAR>h : IsPrimitiveRoot μ ↑n<GOAL>CyclotomicRing n A K = ↥(adjoin A {μ})
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>μ : CyclotomicField n K<VAR>h : IsPrimitiveRoot μ ↑n<GOAL>CyclotomicRing n A K = ↥(adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1})
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Mul α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ s t u : Finset α<GOAL>(filter (fun x => match x with | (a, b) => a * b ∈ u) (s ×ˢ t)).card ^ 2 ≤ u.card * Eₘ[s, t]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>w : σ → M<VAR>n✝ : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝ : DecidableEq M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>h : p ∈ weightedHomogeneousSubmodule R w n<GOAL>(weightedHomogeneousComponent w m) p = if m = n then p else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>w : σ → M<VAR>n✝ : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝ : DecidableEq M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>h : IsWeightedHomogeneous w p n<GOAL>(weightedHomogeneousComponent w m) p = if m = n then p else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>w : σ → M<VAR>n✝ : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝ : DecidableEq M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>h : IsWeightedHomogeneous w p n<VAR>x : σ →₀ ℕ<GOAL>coeff x ((weightedHomogeneousComponent w m) p) = coeff x (if m = n then p else 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>w : σ → M<VAR>n✝ : M<VAR>φ ψ : MvPolynomial σ R<VAR>inst✝ : DecidableEq M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>h : IsWeightedHomogeneous w p n<VAR>x : σ →₀ ℕ<GOAL>(if (weight w) x = m then coeff x p else 0) = coeff x (if m = n then p else 0)
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 ≤ x<VAR>h_one_le : 1 ≤ z<GOAL>x ≤ x ^ z
<VAR>x : ℝ≥0∞<VAR>z : ℝ<VAR>hx : 1 ≤ x<VAR>h_one_le : 1 ≤ z<GOAL>x ^ 1 ≤ x ^ z
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ (1 / z) ↔ x ^ z ≤ y
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group H<VAR>inst✝¹ : MulAction G α<VAR>a : G<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>a ∈ stabilizer G s ↔ a • s ⊆ s
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>h : y ≠ 0<GOAL>cons y s ≠ 0
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>c : cons y s = 0<GOAL>y = 0
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ b<GOAL>a * b ≤ max a b
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<GOAL>Continuous fun a => ‖a‖
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<GOAL>False
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<VAR>p : Subspace k E<VAR>hp : p ∈ s<VAR>hfi : (Submodule.toAddSubgroup p).FiniteIndex<GOAL>False
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<VAR>p : Subspace k E<VAR>hp : p ∈ s<VAR>hfi : (Submodule.toAddSubgroup p).FiniteIndex<VAR>this : Finite (E ⧸ p)<GOAL>False
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<VAR>p : Subspace k E<VAR>hp : p ∈ s<VAR>hfi : (Submodule.toAddSubgroup p).FiniteIndex<VAR>this✝ : Finite (E ⧸ p)<VAR>this : Nontrivial (E ⧸ p)<GOAL>False
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : Infinite k<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module k E<VAR>s : Finset (Subspace k E)<VAR>hs : ∀ p ∈ s, p ≠ ⊤<VAR>hcovers : ⋃ p ∈ s, ↑p = Set.univ<VAR>p : Subspace k E<VAR>hp : p ∈ s<VAR>hfi : (Submodule.toAddSubgroup p).FiniteIndex<VAR>this✝¹ : Finite (E ⧸ p)<VAR>this✝ : Nontrivial (E ⧸ p)<VAR>this : Infinite (E ⧸ p)<GOAL>False
<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>1 < a * b⁻¹ ↔ b < a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ C<VAR>c : (k : K) → ColimitCocone (F.flip.obj k)<VAR>j₁ j₂ : J<VAR>g : j₁ ⟶ j₂<VAR>k : K<GOAL>(F.map g ≫ (fun j => { app := fun k => (c k).cocone.ι.app j, naturality := ⋯ }) j₂).app k = ((fun j => { app := fun k => (c k).cocone.ι.app j, naturality := ⋯ }) j₁ ≫ ((const J).obj { obj := fun k => (c k).cocone.pt, map := fun {k₁ k₂} f => (c k₁).isColimit.desc { pt := (c k₂).cocone.pt, ι := F.flip.map f ≫ (c k₂).cocone.ι }, map_id := ⋯, map_comp := ⋯ }).map g).app k
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>g : G<VAR>hg : g ≠ 1<VAR>hp : Fact (Nat.Prime (Fintype.card G))<GOAL>zpowers g = ⊤
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>g : G<VAR>hg : g ≠ 1<VAR>hp : Fact (Nat.Prime (Fintype.card G))<VAR>this : zpowers g = ⊥ ∨ zpowers g = ⊤<GOAL>zpowers g = ⊤
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<GOAL>c⁻¹ * a < b ↔ a < b * c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ C : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<GOAL>(A * B * C).card * A.card ≤ (A * B).card * (A * C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<GOAL>(A * B * ∅).card * A.card ≤ (A * B).card * (A * ∅).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<GOAL>(A * B * insert x C).card * A.card ≤ (A * B).card * (A * insert x C).card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<GOAL>(A * B * C').card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<GOAL>(A * B * C').card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<GOAL>(A * B * C').card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<VAR>h₂ : A' * B * {x} ⊆ A * B * {x}<GOAL>(A * B * C').card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<VAR>h₂ : A' * B * {x} ⊆ A * B * {x}<VAR>h₃ : (A * B * C').card ≤ (A * B * C).card + (A * B).card - (A' * B).card<GOAL>(A * B * C').card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<VAR>h₂ : A' * B * {x} ⊆ A * B * {x}<VAR>h₃ : (A * B * C').card ≤ (A * B * C).card + (A * B).card - (A' * B).card<GOAL>((A * B * C).card + (A * B).card - (A' * B).card) * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<VAR>h₂ : A' * B * {x} ⊆ A * B * {x}<VAR>h₃ : (A * B * C').card ≤ (A * B * C).card + (A * B).card - (A' * B).card<GOAL>(A * B * C).card * A.card + (A * B).card * A.card - (A' * B).card * A.card ≤ (A * B).card * (A * C').card
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B C✝ : Finset α<VAR>hA : ∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card<VAR>x : α<VAR>C : Finset α<VAR>a✝ : x ∉ C<VAR>ih : (A * B * C).card * A.card ≤ (A * B).card * (A * C).card<VAR>A' : Finset α := A ∩ (A * C / {x})<VAR>hA' : A' = A ∩ (A * C / {x})<VAR>C' : Finset α := insert x C<VAR>hC' : C' = insert x C<VAR>h₀ : A' * {x} = A * {x} ∩ (A * C)<VAR>h₁ : A * B * C' = A * B * C ∪ (A * B * {x}) \ (A' * B * {x})<VAR>h₂ : A' * B * {x} ⊆ A * B * {x}<VAR>h₃ : (A * B * C').card ≤ (A * B * C).card + (A * B).card - (A' * B).card<GOAL>(A * B).card * (A * C).card + (A * B).card * A.card - (A * B).card * (A ∩ (A * C / {x})).card = (A * B).card * (A * C').card
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>𝓕 : Set α<VAR>h𝓕 : IsFundamentalDomain G 𝓕 ν<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>this : HasFundamentalDomain G α ν<GOAL>Measure.map (Quotient.mk α_mod_G) (ν.restrict 𝓕) = μ
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>W X Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>Z : C<GOAL>(f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z
<VAR>c : Cardinal.{u_1}<VAR>co : ℵ₀ ≤ c<GOAL>c.ord.IsLimit
<VAR>c : Cardinal.{u_1}<VAR>co : ℵ₀ ≤ c<VAR>h : c.ord = 0<GOAL>ℵ₀ = 0
<VAR>c : Cardinal.{u_1}<VAR>co : ℵ₀ ≤ c<VAR>a : Ordinal.{u_1}<VAR>h : c.ord ≤ succ a<GOAL>c.ord ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝² : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → E<VAR>hf : AEStronglyMeasurable f ((κ ⊗ₖ η) a)<GOAL>Integrable f ((κ ⊗ₖ η) a) ↔ (∀ᵐ (x : β) ∂κ a, Integrable (fun y => f (x, y)) (η (a, x))) ∧ Integrable (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>-x ‖ -y ↔ x ‖ y
<VAR>m : ℕ<GOAL>1 < ack (m + 1 + 1) 0
<VAR>m : ℕ<GOAL>1 < ack (m + 1) 1
<VAR>m n : ℕ<GOAL>1 < ack (m + 1 + 1) (n + 1)
<VAR>m n : ℕ<GOAL>1 < ack (m + 1) (ack (m + 1 + 1) n)
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ s.direction ↔ ∃ p2 ∈ s, v = p2 -ᵥ p
<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>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hp : p ∈ s<VAR>v : V<GOAL>v ∈ (fun x => x -ᵥ p) '' ↑s ↔ ∃ p2 ∈ s, v = p2 -ᵥ p
<VAR>ι : Type u<VAR>ι' : Type w<VAR>f : ι → Cardinal.{v}<VAR>g : ι' → Cardinal.{v}<GOAL>(⨆ i, f i) * ⨆ j, g j = ⨆ i, ⨆ j, f i * g j
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<GOAL>(cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<VAR>h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))<GOAL>(cfcₙAux ⋯ a ha) f ∈ NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A)
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<VAR>h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))<GOAL>(cfcₙAux ⋯ a ha) f ∈ ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<VAR>h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))<GOAL>⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}) ⊆ ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NonUnitalNormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : IsScalarTower 𝕜 A A<VAR>inst✝² : SMulCommClass 𝕜 A A<VAR>inst✝¹ : StarModule 𝕜 A<VAR>p : A → Prop<VAR>p₁ : Unitization 𝕜 A → Prop<VAR>hp₁ : ∀ {x : A}, p₁ ↑x ↔ p x<VAR>a : A<VAR>ha : p a<VAR>inst✝ : ContinuousFunctionalCalculus 𝕜 p₁<VAR>f : C(↑(σₙ 𝕜 a), 𝕜)₀<VAR>h₁ : (cfcₙAux ⋯ a ha) f ∈ closure (⇑(cfcₙAux ⋯ a ha) '' ↑(NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id ⋯}))<GOAL>IsClosed ↑(NonUnitalStarAlgHom.range (Unitization.inrNonUnitalStarAlgHom 𝕜 A))
<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>inst✝ : DecidableEq ι<VAR>p : ι → P<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>c : k<GOAL>(affineCombination k s p) (affineCombinationLineMapWeights i j c) = (AffineMap.lineMap (p i) (p j)) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a : α<GOAL>map f (s.erase a) = (map f s).erase (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a : α<GOAL>image (⇑f) (s.erase a) = (image (⇑f) s).erase (f a)
<VAR>θ ψ : Angle<VAR>h : θ.sign = ψ.sign<GOAL>θ = ψ ↔ |θ.toReal| = |ψ.toReal|
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>H : l.Nodup<VAR>i : Fin l.length<GOAL>(fun x => ⟨indexOf (↑x) l, ⋯⟩) ((fun i => ⟨l.get i, ⋯⟩) i) = i
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : IsAlgClosure F E<VAR>H : IsPurelyInseparable F E<GOAL>IsSepClosed F