ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>p : G.Walk u v<VAR>q : G.Walk v w<GOAL>(p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>0 < normSq z ↔ z ≠ 0
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<GOAL>a ≡ b [PMOD p] ↔ ∃ z, b = a + z • p
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>b : Bicone f<VAR>j j' : J<GOAL>(fun j => F.map (b.ι j)) j ≫ (fun j => F.map (b.π j)) j' = if h : j = j' then eqToHom ⋯ else 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>b : Bicone f<VAR>j j' : J<GOAL>F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
<VAR>ι : Type u_1<VAR>I : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : I → Type u_6<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝¹ : One γ<VAR>inst✝ : LE γ<VAR>f : α → β<VAR>g : α → γ<VAR>e : β → γ<VAR>hg : 1 ≤ g<VAR>he : 1 ≤ e<VAR>_b : β<GOAL>1 _b ≤ extend f g e _b
<GOAL>Tendsto tan (𝓝[<] (π / 2)) atTop
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hPz : P z = 0<GOAL>W'.negAddY P Q = (P x * Q z) ^ 3 * W'.negY Q
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.127674, u_2} D<VAR>inst✝² : Category.{?u.127678, u_3} E<VAR>X : C<VAR>S : Presieve X<VAR>inst✝¹ : S.regular<VAR>inst✝ : Projective X<VAR>F : Cᵒᵖ ⥤ Type u_4<GOAL>IsSheafFor F S
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.127674, u_2} D<VAR>inst✝² : Category.{?u.127678, u_3} E<VAR>X : C<VAR>inst✝¹ : Projective X<VAR>F : Cᵒᵖ ⥤ Type u_4<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>inst✝ : (ofArrows (fun x => Y) fun x => f).regular<GOAL>IsSheafFor F (ofArrows (fun x => Y) fun x => f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Category.{?u.127674, u_2} D<VAR>inst✝² : Category.{?u.127678, u_3} E<VAR>X : C<VAR>inst✝¹ : Projective X<VAR>F : Cᵒᵖ ⥤ Type u_4<VAR>Y : C<VAR>f : Y ⟶ X<VAR>hf : EffectiveEpi f<VAR>inst✝ : (ofArrows (fun x => Y) fun x => f).regular<GOAL>∀ (x : Unit → F.obj (op Y)), Arrows.Compatible F (fun x => f) x → ∃! t, ∀ (i : Unit), F.map f.op t = x i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>v : V<GOAL>op ((toBaseChange A Q) (reverse ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v)))) = (Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)) ((Algebra.TensorProduct.map (↑(AlgEquiv.toOpposite A A)) reverseOp) ((toBaseChange A Q) ((ι (QuadraticForm.baseChange A Q)) (1 ⊗ₜ[R] v))))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>V : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Module R V<VAR>inst✝² : Module A V<VAR>inst✝¹ : IsScalarTower R A V<VAR>inst✝ : Invertible 2<VAR>Q : QuadraticForm R V<VAR>v : V<GOAL>op (1 ⊗ₜ[R] (ι Q) v) = op (unop (↑(AlgEquiv.toOpposite A A) 1) ⊗ₜ[R] unop (op ((ι Q) v)))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<VAR>x✝ : ℤ<GOAL>x✝ ∈ Int.cast ⁻¹' Ioi a ↔ x✝ ∈ Ioi ⌊a⌋
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s' s : Cycle α<VAR>h : s.Nodup<VAR>x : α<VAR>hx : x ∉ s<GOAL>(s.formPerm h) x = x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s s' : Cycle α<VAR>x : α<VAR>a✝ : List α<VAR>h : Nodup (Quot.mk Setoid.r a✝)<VAR>hx : x ∉ Quot.mk Setoid.r a✝<GOAL>(formPerm (Quot.mk Setoid.r a✝) h) x = x
<VAR>M' : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : M → P<VAR>X : Type u_5<VAR>inst✝⁴ : SMul M X<VAR>inst✝³ : SMul M' X<VAR>Y : Type u_6<VAR>inst✝² : SMul N Y<VAR>inst✝¹ : SMul M' Y<VAR>Z : Type u_7<VAR>inst✝ : SMul P Z<VAR>f : X →ₑ[φ] Y<VAR>x : X<GOAL>((MulActionHom.id N).comp f) x = f x
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x y ≤ dist z x + dist z y
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x y ≤ dist x z + dist z y
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin 1 → ℂ) → E<VAR>c : Fin 1 → ℂ<VAR>R : Fin 1 → ℝ<GOAL>(∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin 1 → ℂ) → E<VAR>c : Fin 1 → ℂ<VAR>R : Fin 1 → ℝ<VAR>H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)<GOAL>(∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin 1 → ℂ) → E<VAR>c : Fin 1 → ℂ<VAR>R : Fin 1 → ℝ<VAR>H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)<VAR>H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)<GOAL>(∯ (x : Fin 1 → ℂ) in T(c, R), f x) = ∮ (z : ℂ) in C(c 0, R 0), f fun x => z
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin 1 → ℂ) → E<VAR>c : Fin 1 → ℂ<VAR>R : Fin 1 → ℝ<VAR>H₁ : (⇑(MeasurableEquiv.funUnique (Fin 1) ℝ).symm ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π)<VAR>H₂ : torusMap c R = fun θ x => circleMap (c 0) (R 0) (θ 0)<GOAL>∫ (x : ℝ) in Icc 0 (2 * π), (∏ i : Fin 1, ↑(R i) * cexp (↑((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x i) * I) * I) • f ((fun θ x => circleMap (c 0) (R 0) (θ 0)) ((MeasurableEquiv.funUnique (Fin 1) ℝ).symm x)) = ∫ (x : ℝ) in Icc 0 (2 * π), deriv (circleMap (c 0) (R 0)) x • f fun x_1 => circleMap (c 0) (R 0) x ∂volume
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f✝ : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>f : α × β → StieltjesFunction<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>x : ℝ<GOAL>∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>x : A<GOAL>IsUnit ((Algebra.lmul R A) x) ↔ IsUnit x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>x : A<GOAL>IsUnit x ↔ Function.Bijective ⇑((Algebra.lmul R A) x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>c : ℂ<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<VAR>h0 : f x ∈ slitPlane<GOAL>HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Ordinal.{u_2}<VAR>h : b ≠ 0<GOAL>(a + b).cof = b.cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : Ordinal.{u_2}<VAR>h : 0 ≠ 0<GOAL>(a + 0).cof = cof 0
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a c : Ordinal.{u_2}<VAR>h : succ c ≠ 0<GOAL>(a + succ c).cof = (succ c).cof
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : Ordinal.{u_2}<VAR>h : b ≠ 0<VAR>hb : b.IsLimit<GOAL>(a + b).cof = b.cof
<VAR>x y : ℝ≥0<GOAL>sqrt x = 1 ↔ x = 1
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>a.get i * a.get j ∈ FP a
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>a.get i * a.get j ∈ FP (Stream'.drop i a)
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>(Stream'.drop i a).head * a.get j ∈ FP (Stream'.drop i a)
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<GOAL>FP (Stream'.drop i a).tail (a.get j)
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<VAR>d : ℕ<VAR>hd : j = i.succ + d<GOAL>FP (Stream'.drop i a).tail (a.get j)
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<VAR>d : ℕ<VAR>hd : j = i.succ + d<GOAL>a.get j ∈ FP (Stream'.drop i a).tail
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<VAR>d : ℕ<VAR>hd : j = i.succ + d<VAR>this : (Stream'.drop i a).tail.get d ∈ FP (Stream'.drop i a).tail<GOAL>a.get j ∈ FP (Stream'.drop i a).tail
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<VAR>d : ℕ<VAR>hd : j = i.succ + d<VAR>this : a.get (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))<GOAL>a.get j ∈ FP (Stream'.drop i a).tail
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>a : Stream' M<VAR>i j : ℕ<VAR>ij : i < j<VAR>d : ℕ<VAR>hd : j = i.succ + d<VAR>this : a.get (d + 1 + i) ∈ FP (Stream'.drop 1 (Stream'.drop i a))<GOAL>j = d + 1 + i
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hc : c ≠ 0<VAR>h : c * a = b<GOAL>a = b / c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>c : β<GOAL>Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOn F (fun x => c) p s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>c : β<GOAL>Tendsto (↿F) (p ×ˢ 𝓟 s) (𝓝 c) ↔ TendstoUniformlyOnFilter F (fun x => c) p (𝓟 s)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<GOAL>(MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<GOAL>∀ i ∈ φ.support, ((fun s a => f a * s.prod fun n e => g n ^ e) i (φ i)).IsHomogeneous (n * m)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<VAR>i : σ →₀ ℕ<VAR>hi : i ∈ φ.support<GOAL>((fun s a => f a * s.prod fun n e => g n ^ e) i (φ i)).IsHomogeneous (n * m)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<VAR>i : σ →₀ ℕ<VAR>hi : i ∈ φ.support<GOAL>((fun s a => f a * s.prod fun n e => g n ^ e) i (φ i)).IsHomogeneous (0 + n * m)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<VAR>i : σ →₀ ℕ<VAR>hi : i ∈ φ.support<GOAL>(i.prod fun n e => g n ^ e).IsHomogeneous (n * m)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<VAR>i : σ →₀ ℕ<VAR>hi : i ∈ φ.support<GOAL>n * m = ∑ i_1 ∈ i.support, n * i i_1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<VAR>i : σ →₀ ℕ<VAR>hi : i ∈ φ.support<GOAL>∀ i_1 ∈ i.support, ((fun n e => g n ^ e) i_1 (i i_1)).IsHomogeneous ((fun k => n * i k) i_1)
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>Submonoid.closure (Set.range fun i => swap i.castSucc i.succ) = ⊤
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>⊤ ≤ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<GOAL>{σ | σ.IsSwap} ⊆ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>ih : i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))<VAR>ne : i ≠ j.succ<VAR>lt : i < j.succ<GOAL>swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>ih : i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))<VAR>ne : i ≠ j.succ<VAR>lt : i < j.succ<VAR>mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)<GOAL>swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>j : Fin n<VAR>mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)<VAR>ih : j.castSucc ≠ j.castSucc → j.castSucc < j.castSucc → swap j.castSucc j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))<VAR>ne : j.castSucc ≠ j.succ<VAR>lt : j.castSucc < j.succ<GOAL>swap j.castSucc j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>ih : i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))<VAR>ne : i ≠ j.succ<VAR>lt : i < j.succ<VAR>mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)<VAR>lts : i < j.castSucc<GOAL>swap i j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>α : Type u<VAR>inst✝ : DecidableEq α<VAR>β : Type v<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>ih : i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))<VAR>ne : i ≠ j.succ<VAR>lt : i < j.succ<VAR>mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i => swap i.castSucc i.succ)<VAR>lts : i < j.castSucc<GOAL>swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈ ↑(Submonoid.closure (Set.range fun i => swap i.castSucc i.succ))
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<GOAL>∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>k_mem : k ∈ 𝓝 x<GOAL>∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>k_mem : k ∈ 𝓝 x<VAR>f : C(X, ℝ)<VAR>fk : EqOn (⇑f) 1 k<VAR>f_comp : HasCompactSupport ⇑f<VAR>hf : ∀ (x : X), f x ∈ Icc 0 1<GOAL>∃ f, HasCompactSupport ⇑f ∧ 0 ≤ ⇑f ∧ f x ≠ 0
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>k_mem : k ∈ 𝓝 x<VAR>f : C(X, ℝ)<VAR>fk : EqOn (⇑f) 1 k<VAR>f_comp : HasCompactSupport ⇑f<VAR>hf : ∀ (x : X), f x ∈ Icc 0 1<GOAL>f x ≠ 0
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>k_mem : k ∈ 𝓝 x<VAR>f : C(X, ℝ)<VAR>fk : EqOn (⇑f) 1 k<VAR>f_comp : HasCompactSupport ⇑f<VAR>hf : ∀ (x : X), f x ∈ Icc 0 1<VAR>this : f x = 1 x<GOAL>f x ≠ 0
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>inst✝ : LocallyCompactSpace X<VAR>x : X<VAR>k : Set X<VAR>hk : IsCompact k<VAR>k_mem : k ∈ 𝓝 x<VAR>f : C(X, ℝ)<VAR>fk : EqOn (⇑f) 1 k<VAR>f_comp : HasCompactSupport ⇑f<VAR>hf : ∀ (x : X), f x ∈ Icc 0 1<VAR>this : f x = 1<GOAL>f x ≠ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>1 ≤ ⌈a⌉₊ ↔ 0 < a
<VAR>G H : PGame<VAR>inst✝¹ : G.Impartial<VAR>inst✝ : H.Impartial<VAR>n m : ℕ<VAR>hG : G.grundyValue = ↑n<VAR>hH : H.grundyValue = ↑m<GOAL>(G + H).grundyValue = ↑(n ^^^ m)
<VAR>G H : PGame<VAR>inst✝¹ : G.Impartial<VAR>inst✝ : H.Impartial<VAR>n m : ℕ<VAR>hG : G.grundyValue = ↑n<VAR>hH : H.grundyValue = ↑m<GOAL>G + H ≈ nim ↑(n ^^^ m)
<VAR>G H : PGame<VAR>inst✝¹ : G.Impartial<VAR>inst✝ : H.Impartial<VAR>n m : ℕ<VAR>hG : G.grundyValue = ↑n<VAR>hH : H.grundyValue = ↑m<GOAL>G + H ≈ nim ↑n + nim ↑m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a✝ a' : α<VAR>b : M<VAR>a : α<VAR>b₁ b₂ : M<VAR>eq : single a b₁ = single a b₂<VAR>this : (single a b₁) a = (single a b₂) a<GOAL>b₁ = b₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a ≤ b * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>hb : 0 < b<GOAL>a = 1 * a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizedGCDMonoid α<VAR>s s₁ s₂ : Finset β<VAR>f : β → α<GOAL>normalize (s.lcm f) = s.lcm f
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<GOAL>(List.map f (a :: s)).prod = ∏ m ∈ (a :: s).toFinset, f m ^ count m (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<GOAL>f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<VAR>has : a ∉ s.toFinset<GOAL>f a * ∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ insert a s.toFinset, f x ^ count x (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<VAR>has : a ∉ s.toFinset<GOAL>f a * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<VAR>has : a ∉ s.toFinset<GOAL>∏ m ∈ s.toFinset, f m ^ count m s = ∏ x ∈ s.toFinset, f x ^ count x (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<VAR>has : a ∉ s.toFinset<VAR>x : α<VAR>hx : x ∈ s.toFinset<GOAL>f x ^ count x s = f x ^ count x (a :: s)
<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>M : Type u_6<VAR>inst✝ : CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : List α<VAR>IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s<VAR>has : a ∉ s.toFinset<VAR>x : α<VAR>hx : x ∈ s.toFinset<GOAL>x ≠ a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hcont : ContinuousOn f (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x<GOAL>∀ x ∈ Icc a b, f x = f a
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>hcont : ContinuousOn f (Icc a b)<VAR>hderiv : ∀ x ∈ Ico a b, HasDerivWithinAt f 0 (Ici x) x<VAR>this : ∀ x ∈ Icc a b, ‖f x - f a‖ ≤ 0 * (x - a)<GOAL>∀ x ∈ Icc a b, f x = f a
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CommGroup α<VAR>e : α<VAR>x : Finset α × Finset α<GOAL>x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2