ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ × ℝ → E<VAR>B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p => LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])<VAR>A : ∀ p ∈ polarCoord.symm.source, HasFDerivAt (↑polarCoord.symm) (B p) p<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ × ℝ → E<VAR>B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p => LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])<VAR>A : ∀ p ∈ polarCoord.symm.source, HasFDerivAt (↑polarCoord.symm) (B p) p<VAR>B_det : ∀ (p : ℝ × ℝ), (B p).det = p.1<GOAL>∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p) = ∫ (p : ℝ × ℝ), f p
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : ℝ × ℝ → E<VAR>B : ℝ × ℝ → ℝ × ℝ →L[ℝ] ℝ × ℝ := fun p => LinearMap.toContinuousLinearMap ((Matrix.toLin (Basis.finTwoProd ℝ) (Basis.finTwoProd ℝ)) !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2])<VAR>A : ∀ p ∈ polarCoord.symm.source, HasFDerivAt (↑polarCoord.symm) (B p) p<VAR>B_det : ∀ (p : ℝ × ℝ), (B p).det = p.1<GOAL>∫ (p : ℝ × ℝ), f p = ∫ (p : ℝ × ℝ) in polarCoord.target, p.1 • f (↑polarCoord.symm p)
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).numDenom = (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q), C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p q : K[X]<VAR>hq : q ≠ 0<GOAL>∀ (p : K[X]), (if 0 = 0 then (0, 1) else let r := gcd p 0; (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) = if 1 = 0 then (0, 1) else let r := gcd 0 1; (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p✝ q : K[X]<VAR>hq : q ≠ 0<VAR>p : K[X]<GOAL>(if 0 = 0 then (0, 1) else let r := gcd p 0; (C (0 / r).leadingCoeff⁻¹ * (p / r), C (0 / r).leadingCoeff⁻¹ * (0 / r))) = if 1 = 0 then (0, 1) else let r := gcd 0 1; (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>p✝ q : K[X]<VAR>hq : q ≠ 0<VAR>p : K[X]<GOAL>(0, 1) = let r := gcd 0 1; (C (1 / r).leadingCoeff⁻¹ * (0 / r), C (1 / r).leadingCoeff⁻¹ * (1 / r))
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsHomLift f φ<GOAL>f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsHomLift (p.map φ) φ<GOAL>p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : γ → α<VAR>x✝ : List β<GOAL>Forall₂ R (map f []) x✝ ↔ Forall₂ (fun c b => R (f c) b) [] x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>R S : α → β → Prop<VAR>P : γ → δ → Prop<VAR>Rₐ : α → α → Prop<VAR>f : γ → α<VAR>a : γ<VAR>l : List γ<VAR>x✝ : List β<GOAL>Forall₂ R (map f (a :: l)) x✝ ↔ Forall₂ (fun c b => R (f c) b) (a :: l) x✝
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b✝ : ι → M<VAR>inst✝ : Finite ι<VAR>b : Basis ι R M<VAR>N O : Submodule R M<VAR>N_le_O : N ≤ O<GOAL>∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b✝ : ι → M<VAR>inst✝ : Finite ι<VAR>b : Basis ι R M<VAR>N O : Submodule R M<VAR>N_le_O : N ≤ O<VAR>val✝ : Fintype ι<GOAL>∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
<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>κ : Type u_6<VAR>inst✝ : One α<VAR>f : ι → α<VAR>g : ι → α → β<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hg : ∀ (a : ι), g a 1 = 1<GOAL>∏ i ∈ t, g i ((↑s).mulIndicator f i) = ∏ i ∈ s, g i (f i)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x y : FreeGroup α<GOAL>(lift f).range = Subgroup.closure (Set.range f)
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x y : FreeGroup α<GOAL>Subgroup.closure (Set.range f) ≤ (lift f).range
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x y : FreeGroup α<GOAL>Set.range f ⊆ ↑(lift f).range
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>β : Type v<VAR>inst✝ : Group β<VAR>f : α → β<VAR>x y : FreeGroup α<VAR>a : α<GOAL>f a ∈ ↑(lift f).range
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid α<VAR>x : Holor α []<VAR>h : CPRankMax (0 + 1) (x + 0)<GOAL>CPRankMax 1 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>inst✝ : CommMonoid γ<VAR>r : β → γ → Prop<VAR>f : α → β<VAR>g : α → γ<VAR>s : Finset α<VAR>h₁ : r 1 1<VAR>h₂ : ∀ (a : α) (b : β) (c : γ), r b c → r (f a * b) (g a * c)<GOAL>r (Multiset.map (fun x => f x) s.val).prod (Multiset.map (fun x => g x) s.val).prod
<VAR>a : Cardinal.{v}<GOAL>toENat (lift.{u, v} a) = toENat a
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedRing R<VAR>inst✝ : Archimedean R<VAR>hr : r < 0<VAR>hf : Tendsto f l atBot<GOAL>Tendsto (fun x => f x * r) l atTop
<VAR>v : Vector ℕ (Nat.succ 0 + 1)<GOAL>Nat.rec v.tail.head (fun y IH => IH + 1) v.head = v.head + v.tail.head
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M'<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun x => R) ℕ) fun i => LinearMap.id.smulRight (v i)) = ⊥
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => a * x) ⁻¹' {b} = {a⁻¹ * b}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>hf : f.Monic<GOAL>(AdjoinRoot.isAdjoinRootMonic f hf).root = root f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : BEq α<VAR>inst✝ : Hashable α<VAR>m : Imp α β<VAR>h : m.WF<GOAL>m.size = m.buckets.size ∧ m.buckets.WF
<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>μ : Measure (Quotient α_mod_G)<VAR>i : QuotientMeasureEqMeasurePreimage ν μ<VAR>t : Set α<VAR>fund_dom_t : IsFundamentalDomain G t ν<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>μ U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ t)
<VAR>B : Type u₁<VAR>inst✝² : Bicategory B<VAR>C : Type u₂<VAR>inst✝¹ : Bicategory C<VAR>D : Type u₃<VAR>inst✝ : Bicategory D<VAR>F✝ F : Pseudofunctor B C<VAR>a b : B<VAR>f : a ⟶ b<GOAL>F.map f ◁ (F.mapId b).hom = (F.mapComp f (𝟙 b)).inv ≫ F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>i j : ι<VAR>hij : p i = p j<GOAL>p i ∈ (convexHull 𝕜) (p '' {j})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<VAR>p : ι → E<VAR>hc : ConvexIndependent 𝕜 p<VAR>i j : ι<VAR>hij : p i = p j<GOAL>p j ∈ {p j}
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>norm 1 = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h1 : ¬1 ≈ 0<GOAL>norm 1 = 1
<VAR>m k n : Nat<VAR>H1 : m.Coprime k<GOAL>(m ^ n).Coprime k
<VAR>R : Type u_1<VAR>inst✝ : Ring R<GOAL>↑μ * ↑ζ = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝² : Category.{v', u'} A<VAR>inst✝¹ : ConcreteCategory A<VAR>inst✝ : J.WEqualsLocallyBijective A<VAR>X Y : Cᵒᵖ ⥤ A<VAR>f : X ⟶ Y<GOAL>J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → δ<VAR>hf : MeasurableEmbedding f<VAR>g : δ → β<GOAL>Integrable g (Measure.map f μ) ↔ Integrable (g ∘ f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → δ<VAR>hf : MeasurableEmbedding f<VAR>g : δ → β<GOAL>Memℒp g 1 (Measure.map f μ) ↔ Memℒp (g ∘ f) 1 μ
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I J K L : Ideal R✝<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x y : R<GOAL>span {x} ⊔ span {y} = ⊤ ↔ IsCoprime x y
<VAR>R✝ : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>I J K L : Ideal R✝<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x y : R<GOAL>(∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) ↔ IsCoprime x y
<VAR>x : ℂ<VAR>n : ℤ<GOAL>x ^ ↑n = x ^ n
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>m : ℕ<VAR>hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)<VAR>hmp : m < p<VAR>hm₀ : 0 < m<VAR>a b c d : ℕ<VAR>habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>a b c d : ℕ<VAR>hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)<VAR>hmp : 1 < p<VAR>hm₀ : 0 < 1<VAR>habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>m : ℕ<VAR>hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)<VAR>hmp : m < p<VAR>hm₀ : 0 < m<VAR>a b c d : ℕ<VAR>habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>hm₁ : 1 < m<GOAL>∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>m : ℕ<VAR>hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)<VAR>hmp : m < p<VAR>hm₀ : 0 < m<VAR>a b c d : ℕ<VAR>habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>hm₁ : 1 < m<GOAL>False
<VAR>p : ℕ<VAR>hp : Prime p<VAR>this✝ : Fact (Prime p)<VAR>natAbs_iff : ∀ {a b c d : ℤ} {k : ℕ}, a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k<VAR>hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>m : ℕ<VAR>hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)<VAR>hmp : m < p<VAR>hm₀ : 0 < m<VAR>a b c d : ℕ<VAR>habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p<VAR>hm₁ : 1 < m<VAR>this : NeZero m<GOAL>False
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>s : Finset α<VAR>hf : ∀ (a : α), Injective (f a)<VAR>a : α<VAR>ha : a ∈ s<GOAL>t.card ≤ (image₂ f s t).card
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a✝ a' : α<VAR>b b' : β<VAR>c : γ<VAR>s : Finset α<VAR>hf : ∀ (a : α), Injective (f a)<VAR>a : α<VAR>ha : a ∈ s<GOAL>(image₂ f {a} t).card ≤ (image₂ f s t).card
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s : Set X<VAR>hs : s.Finite<GOAL>IsClosed (⋃ x ∈ s, {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>f₁ =o[l] g₁ ↔ f₂ =o[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>j : n<GOAL>star ↑hA.eigenvectorUnitary *ᵥ (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j) = Pi.single j 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>x✝ x : α<VAR>xs : List α<GOAL>(x :: xs).formPerm ((x :: xs).nthLe xs.length ⋯) = x
<VAR>Ω : Type u_1<VAR>inst✝ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>nonzero : μ ≠ 0<VAR>s : Set Ω<GOAL>μ.normalize s = μ.mass⁻¹ * μ s
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>clog b n ≤ clog c n
<VAR>b c n : ℕ<VAR>hc : 1 < c<VAR>hb : c ≤ b<GOAL>n ≤ b ^ clog c n
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r✝ : R[X]<VAR>r : R<VAR>n k : ℕ<GOAL>((X + C r) ^ n).coeff k = r ^ (n - k) * ↑(n.choose k)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r✝ : R[X]<VAR>r : R<VAR>n k : ℕ<GOAL>∑ x ∈ range (n + 1), (lcoeff R k) (X ^ x * C r ^ (n - x) * ↑(n.choose x)) = r ^ (n - k) * ↑(n.choose k)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r✝ : R[X]<VAR>r : R<VAR>n k : ℕ<GOAL>∑ x ∈ range (n + 1), (X ^ x).coeff k * r ^ (n - x) * ↑(n.choose x) = r ^ (n - k) * ↑(n.choose k)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r✝ : R[X]<VAR>r : R<VAR>n k : ℕ<GOAL>∀ b ∈ range (n + 1), b ≠ k → (X ^ b).coeff k * r ^ (n - b) * ↑(n.choose b) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r✝ : R[X]<VAR>r : R<VAR>n k : ℕ<GOAL>k ∉ range (n + 1) → (X ^ k).coeff k * r ^ (n - k) * ↑(n.choose k) = 0
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<VAR>hmd : m.gcd c ∣ m<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<VAR>hmd : m.gcd c ∣ m<VAR>hcd : m.gcd c ∣ c<GOAL>a ≡ b [MOD m / m.gcd c]
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<VAR>hmd : m.gcd c ∣ m<VAR>hcd : m.gcd c ∣ c<GOAL>↑(m / m.gcd c) ∣ ↑b - ↑a
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<VAR>hmd : m.gcd c ∣ m<VAR>hcd : m.gcd c ∣ c<GOAL>↑m / ↑d ∣ ↑c / ↑d * (↑b - ↑a)
<VAR>m n a b c d✝ : ℕ<VAR>hm : 0 < m<VAR>h : c * a ≡ c * b [MOD m]<VAR>d : ℕ := m.gcd c<VAR>hmd : m.gcd c ∣ m<VAR>hcd : m.gcd c ∣ c<GOAL>(↑m / ↑d).gcd (↑c / ↑d) = 1
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>K : Type u_1<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : NumberField K<VAR>b : Basis ι ℚ K<VAR>b' : Basis ι' ℚ K<VAR>h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)<VAR>h' : ∀ (i : ι') (j : ι), IsIntegral ℤ (b'.toMatrix (⇑b) i j)<GOAL>discr ℚ ⇑b = discr ℚ ⇑b'
<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>K : Type u_1<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : Fintype ι'<VAR>inst✝ : NumberField K<VAR>b : Basis ι ℚ K<VAR>b' : Basis ι' ℚ K<VAR>h : ∀ (i : ι) (j : ι'), IsIntegral ℤ (b.toMatrix (⇑b') i j)<VAR>h' : ∀ (i j : ι'), IsIntegral ℤ (b'.toMatrix (⇑(b.reindex (b.indexEquiv b'))) i j)<GOAL>discr ℚ ⇑b = discr ℚ ⇑b'
<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✝ : CommMonoid β<VAR>s : Multiset ι<VAR>r : α → β → Prop<VAR>f : ι → α<VAR>g : ι → β<VAR>h₁ : r 1 1<VAR>h₂ : ∀ ⦃a : ι⦄ ⦃b : α⦄ ⦃c : β⦄, r b c → r (f a * b) (g a * c)<VAR>l : List ι<GOAL>r (map f ⟦l⟧).prod (map g ⟦l⟧).prod
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ ↑F).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>∀ G ⊆ F, G.card ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<GOAL>(⋂₀ ↑I).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset (Set E)<VAR>left✝ : I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.card = finrank 𝕜 E + 1<GOAL>(⋂₀ ↑I).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset (Set E)<VAR>left✝ : I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.card = finrank 𝕜 E + 1<VAR>this : ⋂₀ ↑J ⊆ ⋂₀ ↑I<GOAL>(⋂₀ ↑I).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>F : Finset (Set E)<VAR>h_card : finrank 𝕜 E + 1 ≤ F.card<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_inter : ∀ G ⊆ F, G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset (Set E)<VAR>left✝ : I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.card = finrank 𝕜 E + 1<VAR>this : ⋂₀ ↑J ⊆ ⋂₀ ↑I<GOAL>(⋂₀ ↑J).Nonempty