ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>x y : ↑(ofOpenSubsets U).glued<VAR>e : (fromOpenSubsetsGlue U) x = (fromOpenSubsetsGlue U) y<GOAL>x = y
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>y : ↑(ofOpenSubsets U).glued<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx : x ∈ U i<VAR>e : (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι i) ⟨x, hx⟩) = (fromOpenSubsetsGlue U) y<GOAL>((ofOpenSubsets U).ι i) ⟨x, hx⟩ = y
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx : x ∈ U i<VAR>j : (ofOpenSubsets U).J<VAR>y : ↑(of α)<VAR>hy : y ∈ U j<VAR>e : (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι i) ⟨x, hx⟩) = (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι j) ⟨y, hy⟩)<GOAL>((ofOpenSubsets U).ι i) ⟨x, hx⟩ = ((ofOpenSubsets U).ι j) ⟨y, hy⟩
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx : x ∈ U i<VAR>j : (ofOpenSubsets U).J<VAR>hy : x ∈ U j<GOAL>((ofOpenSubsets U).ι i) ⟨x, hx⟩ = ((ofOpenSubsets U).ι j) ⟨x, hy⟩
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx : x ∈ U i<VAR>j : (ofOpenSubsets U).J<VAR>hy : x ∈ U j<GOAL>(ofOpenSubsets U).Rel ⟨i, ⟨x, hx⟩⟩ ⟨j, ⟨x, hy⟩⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : cofinite ≤ l<GOAL>l.kerᶜ.Countable
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : cofinite ≤ l<VAR>s : ℕ → Set α<VAR>hs : l.HasAntitoneBasis s<GOAL>l.kerᶜ.Countable
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : cofinite ≤ l<VAR>s : ℕ → Set α<VAR>hs : l.HasAntitoneBasis s<GOAL>(⋃ i, (s i)ᶜ).Countable
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 1<VAR>t : L.Term (α ⊕ Fin l)<GOAL>(R.boundedFormula₁ t).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 1<VAR>t : L.Term (α ⊕ Fin l)<GOAL>(RelMap R fun i => realize (Sum.elim v xs) (![t] i)) = RelMap R ![realize (Sum.elim v xs) t]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 1<VAR>t : L.Term (α ⊕ Fin l)<VAR>x✝ : Fin 1<GOAL>realize (Sum.elim v xs) (![t] x✝) = ![realize (Sum.elim v xs) t] x✝
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁴ : NormedField 𝕜<VAR>inst✝²³ : SeminormedAddCommGroup V<VAR>inst✝²² : NormedSpace 𝕜 V<VAR>inst✝²¹ : PseudoMetricSpace P<VAR>inst✝²⁰ : NormedAddTorsor V P<VAR>inst✝¹⁹ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁸ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁷ : PseudoMetricSpace P₁<VAR>inst✝¹⁶ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁵ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁴ : NormedSpace 𝕜 V₁'<VAR>inst✝¹³ : MetricSpace P₁'<VAR>inst✝¹² : NormedAddTorsor V₁' P₁'<VAR>inst✝¹¹ : SeminormedAddCommGroup V₂<VAR>inst✝¹⁰ : NormedSpace 𝕜 V₂<VAR>inst✝⁹ : PseudoMetricSpace P₂<VAR>inst✝⁸ : NormedAddTorsor V₂ P₂<VAR>inst✝⁷ : SeminormedAddCommGroup V₃<VAR>inst✝⁶ : NormedSpace 𝕜 V₃<VAR>inst✝⁵ : PseudoMetricSpace P₃<VAR>inst✝⁴ : NormedAddTorsor V₃ P₃<VAR>inst✝³ : SeminormedAddCommGroup V₄<VAR>inst✝² : NormedSpace 𝕜 V₄<VAR>inst✝¹ : PseudoMetricSpace P₄<VAR>inst✝ : NormedAddTorsor V₄ P₄<VAR>f : P →ᵃⁱ[𝕜] P₂<VAR>f₁ : P₁' →ᵃⁱ[𝕜] P₂<VAR>x y : P<GOAL>nndist (f x) (f y) = nndist x y
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n < x
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>x : ℝ<GOAL>(¬∀ (n : ℕ), 0 < n → x ≤ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n) ↔ ∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n < x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι✝ : Sort x<VAR>κ : ι✝ → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → β<GOAL>l (⨅ i, ⨅ (hi : p i), u (f i hi)) = ⨅ i, ⨅ (hi : p i), f i hi
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>0 ≤ (fderivWithin ℝ f s a) y
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hy : y ∈ posTangentConeAt s a<VAR>hf : ¬DifferentiableWithinAt ℝ f s a<GOAL>0 ≤ 0 y
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>filter (p ^ (n + 1)).Coprime (range (p ^ (n + 1))) = range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>filter (p ^ (n + 1)).Coprime (range (p ^ (n + 1))) = filter (fun x => x ∉ image (fun x => x * p) (range (p ^ n))) (range (p ^ (n + 1)))
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>∀ x ∈ range (p ^ (n + 1)), (p ^ (n + 1)).Coprime x ↔ x ∉ image (fun x => x * p) (range (p ^ n))
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<GOAL>∀ x < p ^ (n + 1), ¬p ∣ x ↔ ∀ (x_1 : ℕ), ¬(x_1 < p ^ n ∧ x_1 * p = x)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n : ℕ<VAR>h1 : Function.Injective fun x => x * p<VAR>h2 : image (fun x => x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))<GOAL>(range (p ^ (n + 1)) \ image (fun x => x * p) (range (p ^ n))).card = p ^ n * (p - 1)
<VAR>L : Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>(RelMap r fun i => ⟦x i⟧) ↔ RelMap r x
<VAR>L : Language<VAR>M : Type u_1<VAR>s : Setoid M<VAR>ps : L.Prestructure s<VAR>n : ℕ<VAR>r : L.Relations n<VAR>x : Fin n → M<GOAL>Quotient.lift (RelMap r) ⋯ (Quotient.finChoice fun i => ⟦x i⟧) ↔ RelMap r x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>f : β → α<VAR>x : α<GOAL>x ∈ closure (range f) ↔ ∀ r > 0, ∃ y, dist x (f y) < r
<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>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝ : IsLocallySurjective J (f₁ ≫ f₂)<GOAL>IsLocallySurjective J f₂
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>x✝¹ x✝ : M<GOAL>2 • ⅟2 • (Q (x✝¹ + x✝) - Q x✝¹ - Q x✝) = polar (⇑Q) x✝¹ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α<VAR>inst✝³ : AddCommSemigroup α<VAR>inst✝² : Sub α<VAR>inst✝¹ : OrderedSub α<VAR>a b c d : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>a + b - (a + c) ≤ b - c
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>h : s ⋖ t<GOAL>∃ a ∉ s, insert a s = t
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a / c = b / c ↔ a = b
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : DivisionMonoid α<VAR>a b c : α<VAR>h : IsUnit c<GOAL>a * c⁻¹ = b * c⁻¹ ↔ a = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f g : β → α<VAR>a : α<GOAL>s.sup (f ⊔ g) = s.sup f ⊔ s.sup g
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>hp : Irreducible p<VAR>x y : ↑(p.rootSet E)<GOAL>∃ g, g • x = y
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>hp : Irreducible p<VAR>x y : ↑(p.rootSet E)<VAR>hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)<GOAL>∃ g, g • x = y
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>hp : Irreducible p<VAR>x y : ↑(p.rootSet E)<VAR>hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)<VAR>hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)<GOAL>∃ g, g • x = y
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Fact (Splits (algebraMap F E) p)<VAR>hp : Irreducible p<VAR>x y : ↑(p.rootSet E)<VAR>hx : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm x)<VAR>hy : p * C p.leadingCoeff⁻¹ = minpoly F ↑((rootsEquivRoots p E).symm y)<VAR>g : p.SplittingField ≃ₐ[F] p.SplittingField<VAR>hg : (fun m => m • ↑((rootsEquivRoots p E).symm x)) g = ↑((rootsEquivRoots p E).symm y)<GOAL>∃ g, g • x = y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>n : ℕ<VAR>a : M<VAR>b : ↥S<GOAL>mk a b ^ n = mk (a ^ n) (b ^ n)
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq σ<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq σ<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>((∑ i ∈ s, f i).support.sup fun s => toMultiset s) ≤ s.sup fun i => (f i).support.sup fun s => toMultiset s
<VAR>n : ℕ<GOAL>((antidiagonal n).bind fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple 1 ni.2)) = map (fun i => ![i.1, i.2]) (antidiagonal n)
<VAR>n : ℕ<GOAL>((antidiagonal n).bind fun ni => [Fin.cons ni.1 ![ni.2]]) = map (fun i => ![i.1, i.2]) (antidiagonal n)
<VAR>n : ℕ<GOAL>((antidiagonal n).bind fun ni => [Fin.cons ni.1 ![ni.2]]) = (antidiagonal n).bind fun x => [![x.1, x.2]]
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<GOAL>(q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs
<VAR>n : ℕ<VAR>hn' : 1 < n<VAR>hq : 0 ≠ 1<GOAL>(0 - 1) ^ φ n < (eval (↑0) (cyclotomic n ℤ)).natAbs
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<VAR>hq' : 1 < q<GOAL>(q - 1) ^ φ n < (eval (↑q) (cyclotomic n ℤ)).natAbs
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<VAR>hq' : 1 < q<GOAL>(↑q - 1) ^ φ n < ↑|eval (↑q) (cyclotomic n ℤ)|
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<VAR>hq' : 1 < q<GOAL>eval (↑q) (cyclotomic n ℝ) ≤ ↑|eval (↑q) (cyclotomic n ℤ)|
<VAR>n q : ℕ<VAR>hn' : 1 < n<VAR>hq : q ≠ 1<VAR>hq' : 1 < q<GOAL>↑|eval (↑q) (cyclotomic n ℤ)| = |(algebraMap ℤ ℝ) (eval (↑q) (cyclotomic n ℤ))|
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix n' n R<VAR>N : Matrix m m' R<GOAL>M * (toMatrix₂ b₁ b₂) B * N = (toMatrix₂ b₁' b₂') (B.compl₁₂ ((toLin b₁' b₁) Mᵀ) ((toLin b₂' b₂) N))
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>h : f.Disjoint g<GOAL>(f * g).support = f.support ∪ g.support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>h : f.Disjoint g<VAR>a : α<GOAL>a ∈ f.support ∪ g.support → a ∈ (f * g).support
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>h : f.Disjoint g<VAR>a : α<GOAL>f (g a) = a → f a = a ∧ g a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p✝ : R[X]<VAR>x : S<VAR>p : R[X]<VAR>n✝ : ℕ<GOAL>(p.leadingCoeff • normalizeScaleRoots p).coeff n✝ = (p.scaleRoots p.leadingCoeff).coeff n✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p✝ : R[X]<VAR>x : S<VAR>p : R[X]<VAR>n✝ : ℕ<GOAL>(if ¬p.coeff n✝ = 0 then if n✝ = p.natDegree then p.leadingCoeff • 1 else p.leadingCoeff • (p.coeff n✝ * p.leadingCoeff ^ (p.natDegree - 1 - n✝)) else 0) = p.coeff n✝ * p.leadingCoeff ^ (p.natDegree - n✝)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f✝ f : R →+* S<VAR>p✝ : R[X]<VAR>x : S<VAR>p : R[X]<VAR>n✝ : ℕ<GOAL>(if p.coeff n✝ = 0 then 0 else if n✝ = p.natDegree then p.leadingCoeff else p.leadingCoeff * (p.coeff n✝ * p.leadingCoeff ^ (p.natDegree - 1 - n✝))) = p.coeff n✝ * p.leadingCoeff ^ (p.natDegree - n✝)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq α'<VAR>f✝ g : (a : α) → β a<VAR>a✝ : α<VAR>b : β a✝<VAR>P : ⦃a : α⦄ → β a → Prop<VAR>f : (a : α) → β a<VAR>a' : α<VAR>v : β a'<VAR>a : α<GOAL>P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<GOAL>dickson 1 1 p = X ^ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>dickson 1 1 p = X ^ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>map (ZMod.castHom ⋯ K) (dickson 1 1 p) = map (ZMod.castHom ⋯ K) (X ^ p)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>dickson 1 ((ZMod.castHom ⋯ K) 1) p = X ^ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>{x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}.Infinite
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>{x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0} ⊆ {x | eval x (dickson 1 ((ZMod.castHom ⋯ K) 1) p) = eval x (X ^ p)}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>K : Type<VAR>w✝¹ : Field K<VAR>w✝ : CharP K p<VAR>H : Infinite K<GOAL>{x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Infinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝ : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<GOAL>a * b = p * (p ^ (n + m) * s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝² : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝¹ : p ∣ a<VAR>x : α<VAR>hx : a = p * x<VAR>hn0 : 0 < n<VAR>x✝ : p ^ (n - 1 + 1) ∣ x<VAR>y : α<VAR>hy : x = p ^ (n - 1 + 1) * y<GOAL>p * x * p = p ^ (n + 1) * y * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝² : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝¹ : p ∣ a<VAR>x : α<VAR>hx : a = p * x<VAR>hn0 : 0 < n<VAR>x✝ : p ^ (n - 1 + 1) ∣ x<VAR>y : α<VAR>hy : x = p ^ n * y<GOAL>p * x * p = p ^ (n + 1) * y * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝¹ : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this✝ : p ∣ a * b<VAR>x✝ : p ∣ a<VAR>x : α<VAR>hx : a = p * x<VAR>hn0 : 0 < n<VAR>hpx : ¬p ^ (n - 1 + 1) ∣ x<VAR>this : 1 ≤ n + m<GOAL>x * b * p = p ^ (n - 1 + m + 1) * s * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝¹ : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this✝ : p ∣ a * b<VAR>x✝ : p ∣ a<VAR>x : α<VAR>hx : a = p * x<VAR>hn0 : 0 < n<VAR>hpx : ¬p ^ (n - 1 + 1) ∣ x<VAR>this : 1 ≤ n + m<GOAL>x * b * p = p ^ (n + m) * s * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝² : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝¹ : p ∣ b<VAR>x : α<VAR>hx : b = p * x<VAR>hm0 : 0 < m<VAR>x✝ : p ^ (m - 1 + 1) ∣ x<VAR>y : α<VAR>hy : x = p ^ (m - 1 + 1) * y<GOAL>p * x * p = p ^ (m + 1) * y * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝² : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝¹ : p ∣ b<VAR>x : α<VAR>hx : b = p * x<VAR>hm0 : 0 < m<VAR>x✝ : p ^ (m - 1 + 1) ∣ x<VAR>y : α<VAR>hy : x = p ^ m * y<GOAL>p * x * p = p ^ (m + 1) * y * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝¹ : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝ : p ∣ b<VAR>x : α<VAR>hx : b = p * x<VAR>hm0 : 0 < m<VAR>hpx : ¬p ^ (m - 1 + 1) ∣ x<GOAL>a * x * p = p ^ (n + (m - 1) + 1) * s * p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<VAR>ha : ¬p ^ (n + 1) ∣ a<VAR>hb : ¬p ^ (m + 1) ∣ b<VAR>x✝¹ : p ^ (n + m + 1) ∣ a * b<VAR>s : α<VAR>hs : a * b = p ^ (n + m + 1) * s<VAR>this : p ∣ a * b<VAR>x✝ : p ∣ b<VAR>x : α<VAR>hx : b = p * x<VAR>hm0 : 0 < m<VAR>hpx : ¬p ^ (m - 1 + 1) ∣ x<GOAL>a * x * p = p ^ (n + m) * s * p
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x b a y : X<VAR>ha : x ⊓ y = a<VAR>hxy : x ≠ y<VAR>hxb : IsMaximal x b<VAR>hyb : IsMaximal y b<GOAL>IsMaximal a y
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x b a y : X<VAR>ha : x ⊓ y = a<VAR>hxy : x ≠ y<VAR>hxb : IsMaximal x b<VAR>hyb : IsMaximal y b<VAR>hb : x ⊔ y = b<GOAL>IsMaximal a y
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>x y : X<VAR>hxy : x ≠ y<VAR>hxb : IsMaximal x (x ⊔ y)<VAR>hyb : IsMaximal y (x ⊔ y)<GOAL>IsMaximal (x ⊓ y) y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered Cᵒᵖ<VAR>inst✝¹ : HasColimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsSeparating 𝒢<GOAL>HasTerminal C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered Cᵒᵖ<VAR>inst✝¹ : HasColimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsSeparating 𝒢<VAR>this : Small.{v₁, u₁} ↑𝒢.op<GOAL>HasTerminal C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : WellPowered Cᵒᵖ<VAR>inst✝¹ : HasColimits C<VAR>𝒢 : Set C<VAR>inst✝ : Small.{v₁, u₁} ↑𝒢<VAR>h𝒢 : IsSeparating 𝒢<VAR>this✝ : Small.{v₁, u₁} ↑𝒢.op<VAR>this : HasInitial Cᵒᵖ<GOAL>HasTerminal C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddCommGroup α<VAR>hf : Periodic f c<VAR>x : α<VAR>m : ℤ<GOAL>f (⟨(fun x => x • c) m, ⋯⟩ +ᵥ x) = f x
<VAR>T : ℝ<GOAL>Continuous { toFun := Angle.expMapCircle, invFun := fun x => ↑(↑x).arg, left_inv := Angle.arg_expMapCircle, right_inv := expMapCircle_arg }.invFun
<VAR>T : ℝ<GOAL>∀ (x : ↥circle), ContinuousAt { toFun := Angle.expMapCircle, invFun := fun x => ↑(↑x).arg, left_inv := Angle.arg_expMapCircle, right_inv := expMapCircle_arg }.invFun x
<VAR>T : ℝ<VAR>x : ↥circle<GOAL>ContinuousAt { toFun := Angle.expMapCircle, invFun := fun x => ↑(↑x).arg, left_inv := Angle.arg_expMapCircle, right_inv := expMapCircle_arg }.invFun x
<VAR>S : ShortComplex Ab<GOAL>S.Exact ↔ Function.Exact ⇑S.f ⇑S.g
<VAR>S : ShortComplex Ab<GOAL>AddMonoidHom.range S.f = AddMonoidHom.ker S.g ↔ AddMonoidHom.ker S.g = AddMonoidHom.range S.f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>π : δ → Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : (a : δ) → MeasurableSpace (π a)<VAR>inst✝ : MeasurableSpace γ<VAR>s : Set δ<VAR>t : (i : δ) → Set (π i)<VAR>hs : s.Countable<VAR>ht : ∀ i ∈ s, MeasurableSet (t i)<GOAL>MeasurableSet (s.pi t)