ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(-{ toFinsupp := toFinsupp✝ }).coeff n = -{ toFinsupp := toFinsupp✝ }.coeff n
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>n : ℕ<VAR>toFinsupp✝ : R[ℕ]<GOAL>(match (motive := R[X] → ℕ → R) { toFinsupp := -toFinsupp✝ } with | { toFinsupp := p } => ⇑p) n = -(match (motive := R[X] → ℕ → R) { toFinsupp := toFinsupp✝ } with | { toFinsupp := p } => ⇑p) n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F✝ : Type u_9<VAR>inst✝⁶ : One M<VAR>inst✝⁵ : One N<VAR>inst✝⁴ : FunLike F✝ M N<VAR>R : Type u_10<VAR>S : Type u_11<VAR>F : Type u_12<VAR>inst✝³ : One R<VAR>inst✝² : One S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : OneHomClass F R S<VAR>f : F<VAR>x : R<VAR>hx : f x ≠ 1<GOAL>f x ≠ f 1
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ∣ Nat.card G<GOAL>p ∣ Nat.card ↥↑P
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ^ 1 ∣ Nat.card G<GOAL>p ∣ Nat.card ↥↑P
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>hdvd : p ^ 1 ∣ Nat.card G<VAR>key : p ^ 1 ∣ Nat.card ↥↑P<GOAL>p ∣ Nat.card ↥↑P
<VAR>p q : ℚ<VAR>hq : 0 ≤ q<GOAL>(p / q).toNNRat = p.toNNRat / q.toNNRat
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>s : Set (CofiniteTopology X)<GOAL>IsOpen s ↔ s = ∅ ∨ sᶜ.Finite
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>h : IsCoatomic αᵒᵈ<VAR>b : α<GOAL>b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : OrderBot α<VAR>h : IsAtomic α<VAR>b : αᵒᵈ<GOAL>b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a
<VAR>x✝ y x : ℝ<GOAL>sin 0 ≤ x ↔ 0 ≤ x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>x y : 𝕎 k<GOAL>peval (polyOfInterest p n) ![fun i => x.coeff i, fun i => y.coeff i] = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>x y : 𝕎 k<GOAL>(x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>x y : 𝕎 k<VAR>this : ↑p = 0<GOAL>(x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) - y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) - x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>x y : 𝕎 k<VAR>this : ↑p = 0<GOAL>(x * y).coeff (n + 1) - y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) - x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝¹ : CommRing k<VAR>inst✝ : CharP k p<VAR>n : ℕ<VAR>x y : 𝕎 k<VAR>this : ↑p = 0<VAR>sum_zero_pow_mul_pow_p : ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)<GOAL>(x * y).coeff (n + 1) - y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) - x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
<VAR>k G : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Group G<VAR>A : Rep k G<VAR>inst✝ : A.IsTrivial<VAR>x✝¹ : CoeSort.coe A<VAR>x✝ : G<GOAL>(dZero A) x✝¹ x✝ = 0 x✝¹ x✝
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u₂<VAR>inst✝² : Category.{u₁, u₂} C<VAR>G : Type u_1<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsPreconnected G<GOAL>∀ (x y : G), Nonempty (x ⟶ y)
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u₂<VAR>inst✝² : Category.{u₁, u₂} C<VAR>G : Type u_1<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsPreconnected G<GOAL>_root_.Equivalence fun x y => Nonempty (x ⟶ y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>(pullbackP1Iso 𝒰 f g i).inv ≫ pullback.snd (p1 𝒰 f g) (𝒰.map i) = pullback.fst (𝒰.map i ≫ f) g
<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✝ : DecidableEq α<VAR>hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1<GOAL>∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>x : 𝕜<VAR>h : MeromorphicAt (-f) x<GOAL>MeromorphicAt f x
<VAR>a : ℝ<GOAL>frontier {z | a < z.im} = {z | z.im = a}
<VAR>R : Type u<VAR>a b : R<VAR>m✝ n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n m : ℕ<VAR>r s : R<GOAL>((monomial n) r * (monomial m) s).toFinsupp = ((monomial (n + m)) (r * s)).toFinsupp
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>f : β ⊕ γ → α<VAR>c : α<GOAL>⨆ x, f x ≤ c ↔ (⨆ i, f (Sum.inl i)) ⊔ ⨆ j, f (Sum.inr j) ≤ c
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : S.HasRightHomology<VAR>inst✝ : HasCokernel S.f<VAR>h : S.RightHomologyData := S.rightHomologyData<VAR>this : HasLimit (parallelPair h.g' 0)<GOAL>HasKernel (cokernel.desc S.f S.g ⋯)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : S.HasRightHomology<VAR>inst✝ : HasCokernel S.f<VAR>h : S.RightHomologyData := S.rightHomologyData<VAR>this : HasLimit (parallelPair h.g' 0)<VAR>e : parallelPair (cokernel.desc S.f S.g ⋯) 0 ≅ parallelPair h.g' 0 := parallelPair.ext ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp) (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)) ⋯ ⋯<GOAL>HasKernel (cokernel.desc S.f S.g ⋯)
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>p q : R[X]<VAR>inst✝ : NoZeroDivisors R<VAR>hp : ¬p = 0<GOAL>(p * p.mirror).natTrailingDegree = 2 * p.natTrailingDegree
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>s : Finset α<VAR>hs : ¬s ⊆ 0<GOAL>↑(s • univ) = ↑univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>s : Finset α<VAR>hs : ¬↑s ⊆ ↑0<GOAL>↑(s • univ) = ↑univ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>s : Finset α<VAR>hs : ¬↑s ⊆ 0<GOAL>↑s • Set.univ = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : PseudoMetricSpace α<VAR>s : Set α<VAR>x y z : α<VAR>inst✝ : ProperSpace α<GOAL>EMetric.diam univ = ⊤ ↔ NoncompactSpace α
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s t✝ : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x✝ →L[𝕜] TangentSpace I' (f x✝)<VAR>g' : TangentSpace I' (f x✝) →L[𝕜] TangentSpace I'' (g (f x✝))<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ MDifferentiableOn I I' f (s ∩ u)<VAR>x : M<VAR>xs : x ∈ s<VAR>t : Set M<VAR>t_open : IsOpen t<VAR>xt : x ∈ t<VAR>ht : MDifferentiableOn I I' f (s ∩ t)<GOAL>MDifferentiableWithinAt I I' f s x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f g : ι → Set X<VAR>h : LocallyFinite f<VAR>x : X<GOAL>x ∈ closure (⋃ i, f i) ↔ x ∈ ⋃ i, closure (f i)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>x y : R<VAR>x✝ : A<GOAL>x✝ ∈ (x * y) • (M * N) ↔ x✝ ∈ x • M * y • N
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>x y : R<VAR>x✝ : A<GOAL>x✝ ∈ (x * y) • (M * N) → x✝ ∈ x • M * y • N
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M N P Q : Submodule R A<VAR>m n : A<VAR>x y : R<VAR>x✝ : A<VAR>hx : x✝ ∈ x • M * y • N<GOAL>∀ m ∈ x • M, ∀ n ∈ y • N, m * n ∈ (x * y) • (M * N)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Ideal.span {C r * X () - 1} = RingHom.ker (aeval (Generators.localizationAway r).val)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>this : aeval (Generators.localizationAway r).val = (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))<GOAL>Ideal.span {C r * X () - 1} = RingHom.ker (aeval (Generators.localizationAway r).val)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>this : aeval (Generators.localizationAway r).val = (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))<GOAL>Ideal.span {C r * X () - 1} = RingHom.ker ((↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1})))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>this : aeval (Generators.localizationAway r).val = (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))<GOAL>Ideal.span {C r * X () - 1} = Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker (↑(mvPolynomialQuotientEquiv S r)).toRingHom)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>this : aeval (Generators.localizationAway r).val = (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))<GOAL>Ideal.span {C r * X () - 1} = Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker ↑(mvPolynomialQuotientEquiv S r))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>P : Presentation R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<VAR>this : aeval (Generators.localizationAway r).val = (↑(mvPolynomialQuotientEquiv S r)).comp (Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))<GOAL>Ideal.span {C r * X () - 1} = Ideal.comap (↑(Ideal.Quotient.mkₐ R (Ideal.span {C r * X () - 1}))) (RingHom.ker (mvPolynomialQuotientEquiv S r))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Monoid α<VAR>n : ℕ<VAR>f : Fin n → α<VAR>j : Fin n<GOAL>partialProd f j.succ = partialProd f j.castSucc * f j
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ ⨆ i, S i<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x₁
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<GOAL>C x₁
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<VAR>x₂ : M<VAR>hx₂ : x₂ ∈ ⋃ i, ↑(S i)<GOAL>C x₂
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>C : M → Prop<VAR>x₁ : M<VAR>hx₁ : x₁ ∈ closure (⋃ i, ↑(S i))<VAR>mem : ∀ (i : ι), ∀ x₂ ∈ S i, C x₂<VAR>mul : ∀ (x y : M), C x → C y → C (x * y)<VAR>x₂ : M<VAR>hx₂ : x₂ ∈ ⋃ i, ↑(S i)<VAR>i : ι<VAR>hi : x₂ ∈ ↑(S i)<GOAL>C x₂
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD 2]
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>n : ℕ<GOAL>2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]
<VAR>ι✝ : Type u<VAR>α : Type v<VAR>inst✝¹ : DecidableEq α<VAR>t✝ : ι✝ → Finset α<VAR>inst✝ : Fintype ι✝<VAR>ι : Type u<VAR>t : ι → Finset α<VAR>s : Finset ι<VAR>ht : ∀ (s : Finset ι), s.card ≤ (s.biUnion t).card<VAR>s' : Finset ↑↑s<GOAL>s'.card ≤ (s'.biUnion fun a' => t ↑a').card
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<GOAL>Sbtw R x y z ↔ x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : Sbtw R x y z<GOAL>z ∈ ⇑(lineMap x y) '' Set.Ioi 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : x ≠ y ∧ z ∈ ⇑(lineMap x y) '' Set.Ioi 1<GOAL>Sbtw R x y z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>jk : k ≥ j<VAR>h₁ : abv (↑(f - g) j) < ε / 2<VAR>h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<GOAL>abv (↑f k - ↑g j) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : CauSeq β abv<VAR>h : f ≈ g<VAR>ε : α<VAR>ε0 : 0 < ε<VAR>i : ℕ<VAR>H : ∀ j ≥ i, abv (↑(f - g) j) < ε / 2 ∧ ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>k : ℕ<VAR>jk : k ≥ j<VAR>h₁ : abv (↑(f - g) j) < ε / 2<VAR>h₂ : ∀ k ≥ j, abv (↑f k - ↑f j) < ε / 2<VAR>this : abv (↑f j - ↑g j + (↑f k - ↑f j)) < ε / 2 + ε / 2<GOAL>abv (↑f k - ↑g j) < ε
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>a b : G<GOAL>a⁻¹ * (b * a) = b
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>X✝ Y Z : C<VAR>f : Y ⟶ X✝<VAR>S R : Sieve X✝<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>F : C ⥤ D<VAR>X : C<GOAL>functorPushforward F ⊤ = ⊤
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>X✝ Y Z : C<VAR>f : Y ⟶ X✝<VAR>S R : Sieve X✝<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>F : C ⥤ D<VAR>X : C<GOAL>generate (functorPushforward F ⊤).arrows = ⊤
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>F✝ : C ⥤ D<VAR>X✝ Y Z : C<VAR>f : Y ⟶ X✝<VAR>S R : Sieve X✝<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>G : D ⥤ E<VAR>F : C ⥤ D<VAR>X : C<GOAL>(functorPushforward F ⊤).arrows (𝟙 (F.obj X))
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>N : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R N<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Qₙ : QuadraticForm R N<VAR>m₁ : M₁<GOAL>(toProd Q₁ Q₂) ((ι Q₁) m₁ ᵍ⊗ₜ[R] 1) = (ι (QuadraticMap.prod Q₁ Q₂)) (m₁, 0)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>l : List α<VAR>a : α<GOAL>↑l = {a} ↔ l = [a]
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<GOAL>vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommSemiring R<GOAL>∀ ⦃a a' : Set (PrimeSpectrum R)⦄, a ∈ {s | IsClosed s ∧ IsIrreducible s} → a' ∈ {s | IsClosed s ∧ IsIrreducible s} → (Function.swap (fun x x_1 => x ≤ x_1) a a' ↔ vanishingIdeal a ≤ vanishingIdeal a')
<VAR>t : Type u → Type u → Type u<VAR>inst✝⁵ : Bitraversable t<VAR>β✝ : Type u<VAR>F G : Type u → Type u<VAR>inst✝⁴ : Applicative F<VAR>inst✝³ : Applicative G<VAR>inst✝² : LawfulBitraversable t<VAR>inst✝¹ : LawfulApplicative F<VAR>inst✝ : LawfulApplicative G<VAR>α β β' : Type u<VAR>f : β → β'<VAR>x : t α β<GOAL>tsnd (pure ∘ f) x = pure (snd f x)
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>a : M₀<VAR>m n n✝ m✝ : ℕ<VAR>hmn : n✝.le m✝<VAR>ha : a ^ n✝ = 0<GOAL>a ^ m✝.succ = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>u v w : m → α<GOAL>(u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Kernel α (β × Ω)<VAR>inst✝¹ : IsFiniteKernel ρ<VAR>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<GOAL>(fun b => κ (a, b)) =ᶠ[ae (ρ.fst a)] ⇑(ρ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Kernel α (β × Ω)<VAR>inst✝¹ : IsFiniteKernel ρ<VAR>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<VAR>this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b => (a, b)) ⋯<GOAL>(fun b => κ (a, b)) =ᶠ[ae (ρ.fst a)] ⇑(ρ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Kernel α (β × Ω)<VAR>inst✝¹ : IsFiniteKernel ρ<VAR>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<VAR>this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b => (a, b)) ⋯<VAR>h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b => (a, b)) ⋯) x = (ρ a).condKernel x<GOAL>(fun b => κ (a, b)) =ᶠ[ae (ρ.fst a)] ⇑(ρ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Kernel α (β × Ω)<VAR>inst✝¹ : IsFiniteKernel ρ<VAR>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<VAR>this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b => (a, b)) ⋯<VAR>h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b => (a, b)) ⋯) x = (ρ a).condKernel x<GOAL>(fun b => κ (a, b)) =ᶠ[ae (Measure.map Prod.fst (ρ a))] ⇑(ρ a).condKernel
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>ρ : Kernel α (β × Ω)<VAR>inst✝¹ : IsFiniteKernel ρ<VAR>κ : Kernel (α × β) Ω<VAR>inst✝ : IsFiniteKernel κ<VAR>hκ : ρ.fst ⊗ₖ κ = ρ<VAR>a : α<VAR>this : ρ a = (ρ a).fst ⊗ₘ κ.comap (fun b => (a, b)) ⋯<VAR>h : ∀ᵐ (x : β) ∂(ρ a).fst, (κ.comap (fun b => (a, b)) ⋯) x = (ρ a).condKernel x<VAR>b : β<VAR>hb : (κ.comap (fun b => (a, b)) ⋯) b = (ρ a).condKernel b<GOAL>κ (a, b) = (ρ a).condKernel b
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u_1<VAR>x : (i : Fin (n + 1)) → α i<VAR>s : (i : Fin (n + 1)) → Finset (α i)<GOAL>x ∈ piFinset s ↔ init x ∈ piFinset (init s) ∧ x (last n) ∈ s (last n)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>k : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>ι : Type u_8<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s : R<VAR>x y : M<VAR>zero_eq_one : 0 = 1<GOAL>x = 0
<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>S : L.Substructure M<VAR>s✝ s : Set M<VAR>p : (x : M) → x ∈ (closure L).toFun s → Prop<VAR>Hs : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}<VAR>x : M<VAR>hx : x ∈ (closure L).toFun s<GOAL>p x hx
<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>S : L.Substructure M<VAR>s✝ s : Set M<VAR>p : (x : M) → x ∈ (closure L).toFun s → Prop<VAR>Hs : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}<VAR>x : M<VAR>hx : x ∈ (closure L).toFun s<GOAL>∃ (x_1 : x ∈ (closure L).toFun s), p x x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹³ : Zero β<VAR>inst✝¹² : One β<VAR>inst✝¹¹ : Add β<VAR>inst✝¹⁰ : Mul β<VAR>inst✝⁹ : Neg β<VAR>inst✝⁸ : Sub β<VAR>inst✝⁷ : SMul ℕ β<VAR>inst✝⁶ : SMul ℤ β<VAR>inst✝⁵ : Pow β ℕ<VAR>inst✝⁴ : NatCast β<VAR>inst✝³ : IntCast β<VAR>f : β → α<VAR>hf : Injective f<VAR>inst✝² : Mul α<VAR>inst✝¹ : Add α<VAR>inst✝ : LeftDistribClass α<VAR>add : ∀ (x y : β), f (x + y) = f x + f y<VAR>mul : ∀ (x y : β), f (x * y) = f x * f y<VAR>x y z : β<GOAL>f (x * (y + z)) = f (x * y + x * z)