ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 2<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : Epi (R₁.map' 1 2 ⋯ ⋯)<VAR>hR₂ : R₂.Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<VAR>ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 := homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 ⋯)) ⋯ ⋯ ⋯<GOAL>(ShortComplex.mk ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 0 1 ⋯ ⋯) ((mk₂ ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 ⋯ ⋯) ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 ⋯ ⋯)).map' 1 2 ⋯ ⋯) ⋯).Exact
<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✝ : GroupWithZero G₀<VAR>a b c g h✝ x : G₀<VAR>h : x ≠ 0<VAR>y y' : G₀<VAR>w : (fun y => x * y) y = (fun y => x * y) y'<GOAL>y = y'
<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>N' : Type u_8<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : N' →ₗ[R] M<VAR>x✝¹ x✝ : N'<GOAL>(((associatedHom S) (Q.comp f)) x✝¹) x✝ = ((LinearMap.compl₁₂ ((associatedHom S) Q) f f) x✝¹) x✝
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝³ : Category.{v', u'} D<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>inst✝ : HasLimitsOfShape J C<VAR>i j : K<VAR>F : J ⥤ K ⥤ C<VAR>f : i ⟶ j<GOAL>(limitObjIsoLimitCompEvaluation F i).inv ≫ (limit F).map f = limMap (whiskerLeft F ((evaluation K C).map f)) ≫ (limitObjIsoLimitCompEvaluation F j).inv
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<GOAL>Associated (gcd (a * b) (a * c)) (a * gcd b c)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>b c : α<GOAL>Associated (gcd (0 * b) (0 * c)) (0 * gcd b c)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>ha : a ≠ 0<GOAL>Associated (gcd (a * b) (a * c)) (a * gcd b c)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>d : α<VAR>eq : gcd (a * b) (a * c) = a * d<GOAL>Associated (gcd (a * b) (a * c)) (a * gcd b c)
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>d : α<VAR>eq : gcd (a * b) (a * c) = a * d<GOAL>gcd (a * b) (a * c) ∣ a * gcd b c
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>d : α<VAR>eq : gcd (a * b) (a * c) = a * d<GOAL>a * gcd b c ∣ gcd (a * b) (a * c)
<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>hn : n ≠ 0<VAR>f : (Fin n → ℂ) → E<VAR>c : Fin n → ℂ<GOAL>(∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0
<VAR>a b c d m✝ n k : ℕ<VAR>p q : ℕ → Prop<VAR>motive : (m : ℕ) → n ≤ m → Sort u_1<VAR>refl : motive n ⋯<VAR>le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯<VAR>m : ℕ<VAR>h1 : n ≤ m<VAR>h2 : n + 1 ≤ m<GOAL>leRec (le_succ_of_le ⋯ refl) (fun k h ih => le_succ_of_le ⋯ ih) h2 = leRec refl le_succ_of_le h1
<VAR>f : Code<VAR>k : Cont'<GOAL>contSupp (Cont'.fix f k) = codeSupp f (Cont'.fix f k)
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>hX : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : X.basicOpen s = ⊥<GOAL>s = 0
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>hX : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : X.basicOpen s = ⊥<GOAL>∀ (x : ↥U), (X.sheaf.presheaf.germ x) s = (X.sheaf.presheaf.germ x) 0
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>hX : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : X.basicOpen s = ⊥<VAR>x : ↥U<GOAL>(X.sheaf.presheaf.germ x) s = (X.sheaf.presheaf.germ x) 0
<VAR>X✝ : Scheme<VAR>X : Scheme<VAR>hX : IsReduced X<VAR>U : X.Opens<VAR>s : ↑Γ(X, U)<VAR>hs : X.basicOpen s = ⊥<VAR>x : ↥U<GOAL>(X.sheaf.presheaf.germ x) s = 0
<VAR>R : Type u_1<VAR>inst✝²³ : CommSemiring R<VAR>R₂ : Type u_2<VAR>inst✝²² : CommSemiring R₂<VAR>R₃ : Type u_3<VAR>inst✝²¹ : CommSemiring R₃<VAR>R₄ : Type u_4<VAR>inst✝²⁰ : CommSemiring R₄<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>Q : Type u_8<VAR>Mₗ : Type u_9<VAR>Nₗ : Type u_10<VAR>Pₗ : Type u_11<VAR>Qₗ : Type u_12<VAR>Qₗ' : Type u_13<VAR>inst✝¹⁹ : AddCommMonoid M<VAR>inst✝¹⁸ : AddCommMonoid N<VAR>inst✝¹⁷ : AddCommMonoid P<VAR>inst✝¹⁶ : AddCommMonoid Q<VAR>inst✝¹⁵ : AddCommMonoid Mₗ<VAR>inst✝¹⁴ : AddCommMonoid Nₗ<VAR>inst✝¹³ : AddCommMonoid Pₗ<VAR>inst✝¹² : AddCommMonoid Qₗ<VAR>inst✝¹¹ : AddCommMonoid Qₗ'<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R₂ N<VAR>inst✝⁸ : Module R₃ P<VAR>inst✝⁷ : Module R₄ Q<VAR>inst✝⁶ : Module R Mₗ<VAR>inst✝⁵ : Module R Nₗ<VAR>inst✝⁴ : Module R Pₗ<VAR>inst✝³ : Module R Qₗ<VAR>inst✝² : Module R Qₗ'<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>σ₄₂ : R₄ →+* R₂<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃<VAR>f✝ : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P<VAR>f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ<VAR>x✝¹ : Mₗ<VAR>x✝ : Nₗ<GOAL>((f.compl₁₂ id id) x✝¹) x✝ = (f x✝¹) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>inst✝ : Fintype α<VAR>s : Cycle α<VAR>h : s.Nodup<VAR>hn : s.Nontrivial<GOAL>(s.formPerm h).support = s.toFinset
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>inst✝ : Fintype α<VAR>s : List α<VAR>h : Nodup (Quot.mk Setoid.r s)<VAR>hn : Nontrivial (Quot.mk Setoid.r s)<GOAL>(formPerm (Quot.mk Setoid.r s) h).support = toFinset (Quot.mk Setoid.r s)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s✝ s' : Cycle α<VAR>inst✝ : Fintype α<VAR>s : List α<VAR>h : Nodup (Quot.mk Setoid.r s)<VAR>hn : Nontrivial (Quot.mk Setoid.r s)<GOAL>∀ (x : α), s ≠ [x]
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>s s' : Cycle α<VAR>inst✝ : Fintype α<VAR>x✝ : α<VAR>h : Nodup (Quot.mk Setoid.r [x✝])<VAR>hn : Nontrivial (Quot.mk Setoid.r [x✝])<GOAL>False
<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✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>(pointReflection R (midpoint R x y)) y = x
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>u : Mˣ<VAR>x✝ : IsUnit (a * ↑u)<VAR>v : Mˣ<VAR>hv : ↑v = a * ↑u<GOAL>IsUnit a
<VAR>α : Type u<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝ : Monoid M<VAR>a : M<VAR>u : Mˣ<VAR>x✝ : IsUnit (a * ↑u)<VAR>v : Mˣ<VAR>hv : ↑v = a * ↑u<VAR>this : IsUnit (a * ↑u * ↑u⁻¹)<GOAL>IsUnit a
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Category.{?u.87545, u_1} C<VAR>inst✝⁶ : Category.{?u.87549, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>G : Type u_4<VAR>inst✝³ : AddGroup G<VAR>inst✝² : HasShift C G<VAR>inst✝¹ : F.ShiftSequence M<VAR>inst✝ : F.ShiftSequence G<VAR>X Y : C<VAR>m : G<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n : G<VAR>hnm : n + m = 0<VAR>a a' : G<VAR>ha' : m + a = a'<GOAL>n + a' = a
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Category.{?u.87545, u_1} C<VAR>inst✝⁶ : Category.{?u.87549, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>G : Type u_4<VAR>inst✝³ : AddGroup G<VAR>inst✝² : HasShift C G<VAR>inst✝¹ : F.ShiftSequence M<VAR>inst✝ : F.ShiftSequence G<VAR>X Y : C<VAR>m : G<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n : G<VAR>hnm : n + m = 0<VAR>a a' : G<VAR>ha' : m + a = a'<GOAL>m + n = 0
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>G : Type u_4<VAR>inst✝³ : AddGroup G<VAR>inst✝² : HasShift C G<VAR>inst✝¹ : F.ShiftSequence M<VAR>inst✝ : F.ShiftSequence G<VAR>X Y : C<VAR>m : G<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n : G<VAR>hnm : n + m = 0<VAR>a a' : G<VAR>ha' : m + a = a'<GOAL>(F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' = (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Category.{u_5, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>G : Type u_4<VAR>inst✝³ : AddGroup G<VAR>inst✝² : HasShift C G<VAR>inst✝¹ : F.ShiftSequence M<VAR>inst✝ : F.ShiftSequence G<VAR>X Y : C<VAR>m : G<VAR>f : X ⟶ (shiftFunctor C m).obj Y<VAR>n : G<VAR>hnm : n + m = 0<VAR>a a' : G<VAR>ha' : m + a = a'<VAR>hnm' : m + n = 0<GOAL>(F.shiftIso n a' a ⋯).hom.app X ≫ F.shiftMap f a a' ha' = (F.shift a').map ((shiftFunctor C n).map f ≫ (shiftFunctorCompIsoId C m n ⋯).hom.app Y)
<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✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : Monoid G<VAR>inst✝¹ : Monoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>a : G<GOAL>f (a ^ 0) = f a ^ 0
<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✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : Monoid G<VAR>inst✝¹ : Monoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>a : G<VAR>n : ℕ<GOAL>f (a ^ (n + 1)) = f a ^ (n + 1)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>(f 0 * s.prod fun n e => g n ^ e) = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>r s : R<GOAL>r + s ∈ σ a ↔ r ∈ σ (-↑ₐ s + a)
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<GOAL>K.incl.range = K
<VAR>R : Type u<VAR>L : Type v<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>L₂ : Type w<VAR>inst✝¹ : LieRing L₂<VAR>inst✝ : LieAlgebra R L₂<VAR>f : L →ₗ⁅R⁆ L₂<VAR>K K' : LieSubalgebra R L<VAR>K₂ : LieSubalgebra R L₂<GOAL>K.incl.range.toSubmodule = K.toSubmodule
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h₀ : 0 < i<VAR>hₙ : i < Fin.last n<VAR>j : Fin n<GOAL>{i, j.castSucc, j.succ}.card ≤ n
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h₀ : 0 < ↑i<VAR>hₙ : ↑i < n<GOAL>{i, j.castSucc, j.succ}.card ≤ n
<VAR>i : Fin (2 + 1)<VAR>j : Fin 2<VAR>h₀ : 0 < ↑i<VAR>hₙ : ↑i < 2<GOAL>{i, j.castSucc, j.succ}.card ≤ 2
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h₀ : 0 < ↑i<VAR>hₙ : ↑i < n<VAR>hn : 2 < n<GOAL>{i, j.castSucc, j.succ}.card ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>s.seq t = ⋃ f ∈ s, f '' t
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<GOAL>IsAtom s ↔ ∃ x, s = {x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<GOAL>IsAtom s → ∃ x, s = {x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<GOAL>(s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ x, s = {x}
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<VAR>hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b<VAR>x : α<VAR>hx : x ∈ s<GOAL>∃ x, s = {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G₀ : Type u_3<VAR>inst✝² : DivInvMonoid G₀<VAR>inst✝¹ : TopologicalSpace G₀<VAR>inst✝ : ContinuousMul G₀<VAR>f : α → G₀<VAR>s : Set α<VAR>l : Filter α<VAR>x : G₀<VAR>hf : Tendsto f l (𝓝 x)<VAR>y : G₀<GOAL>Tendsto (fun a => f a / y) l (𝓝 (x / y))
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : ContinuousConstSMul G α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s✝ : Set β<VAR>c : G<VAR>s : Set α<VAR>hs : Dense s<GOAL>Dense (c • s)
<VAR>M : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : Group G<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : ContinuousConstSMul G α<VAR>inst✝ : TopologicalSpace β<VAR>f : β → α<VAR>b : β<VAR>s✝ : Set β<VAR>c : G<VAR>s : Set α<VAR>hs : closure s = univ<GOAL>closure (c • s) = univ
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : HasTrivialRadical R L<VAR>h : IsLieAbelian L<GOAL>Subsingleton L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : HasTrivialRadical R L<VAR>h : ⊥ = ⊤<GOAL>Subsingleton L
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>S : Type u_2<VAR>τ : Type u_3<VAR>x : τ → S<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>p : MvPolynomial σ R<GOAL>(eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>S : Type u_2<VAR>τ : Type u_3<VAR>x : τ → S<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>p : MvPolynomial σ R<GOAL>∀ (a : R), (eval x) (eval₂ f g (C a)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (C a)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>S : Type u_2<VAR>τ : Type u_3<VAR>x : τ → S<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>p : MvPolynomial σ R<GOAL>∀ (p q : MvPolynomial σ R), (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p → (eval x) (eval₂ f g q) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) q → (eval x) (eval₂ f g (p + q)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p + q)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ : σ → R<VAR>S : Type u_2<VAR>τ : Type u_3<VAR>x : τ → S<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>p : MvPolynomial σ R<GOAL>∀ (p : MvPolynomial σ R) (n : σ), (eval x) (eval₂ f g p) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) p → (eval x) (eval₂ f g (p * X n)) = eval₂ ((eval x).comp f) (fun s => (eval x) (g s)) (p * X n)
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<VAR>succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0<GOAL>(if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hle : g ≤ᶠ[l] f<VAR>hfga : f a = g a<VAR>h : IsMaxFilter f l a<GOAL>IsMaxFilter g l a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hle : g ≤ᶠ[l] f<VAR>hfga : f a = g a<VAR>h : IsMaxFilter f l a<VAR>x : α<VAR>hf : f x ≤ f a<VAR>hgf : g x ≤ f x<GOAL>g x ≤ g a
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>f g : α → β<VAR>a : α<VAR>l : Filter α<VAR>hle : g ≤ᶠ[l] f<VAR>hfga : f a = g a<VAR>h : IsMaxFilter f l a<VAR>x : α<VAR>hf : f x ≤ f a<VAR>hgf : g x ≤ f x<GOAL>g x ≤ f a
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>S : Type u_1<VAR>inst✝ : SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ<GOAL>↑q ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b x✝ : α<GOAL>¬(x✝ ∈ s → x✝ ∉ t) ↔ x✝ ∈ s ∧ x✝ ∈ t
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M<GOAL>Set.range (uncurry M'.relation) = Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M<GOAL>Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) = Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M<GOAL>uncurry M'.relation ∘ Prod.map ⇑e ⇑e = ⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M<VAR>i i' : B<GOAL>(uncurry M'.relation ∘ Prod.map ⇑e ⇑e) (i, i') = (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) (i, i')
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>M : CoxeterMatrix B<VAR>e : B ≃ B'<VAR>M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M<GOAL>Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>s \ ⋃ i, t i = ⋂ i, s \ t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : Nonempty ι<VAR>s : Set β<VAR>t : ι → Set β<GOAL>⋂ i, s ∩ (t i)ᶜ = ⋂ i, s \ t i
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b : E<GOAL>‖a * b‖ ≤ ‖a‖ + ‖b‖
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>s : Finset ι<VAR>c : γ<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(mk s (c • x)) i = (c • mk s x) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : (i : ι) → AddMonoid (β i)<VAR>inst✝ : (i : ι) → DistribMulAction γ (β i)<VAR>s : Finset ι<VAR>c : γ<VAR>x : (i : ↑↑s) → β ↑i<VAR>i : ι<GOAL>(if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring R<VAR>inst✝ : DecidableEq σ<VAR>s t : σ<GOAL>(coeff R (single t 1)) (X s) = if t = s then 1 else 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>(pderiv x) (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 - (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) = C W'.a₁ * X y * X z - (C 3 * X x ^ 2 + C (2 * W'.a₂) * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<GOAL>↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 1) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 0) + ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 0)) - (↑3 * X x ^ (3 - 1) * 1 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 1)) * X z ^ 2 + C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 0)) + ((0 * X x + C W'.a₄ * 1) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 0)) + (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 0))) = C W'.a₁ * X y * X z - (3 * X x ^ 2 + 2 * C W'.a₂ * X x * X z ^ 2 + C W'.a₄ * X z ^ 4)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0<GOAL>∫ (x : X), f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0<GOAL>∫ (x : X) in univ, f x ∂μ = ∫ (x : X) in s, f x ∂μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0<GOAL>∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g : G<VAR>a b : α<VAR>h : a = g⁻¹ • b<GOAL>g • a = b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝³ : Monoid M<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : Group G<VAR>inst✝ : MulAction G α<VAR>g : G<VAR>a b : α<VAR>h : g • a = b<GOAL>a = g⁻¹ • b
<VAR>m n : ℤ<GOAL>bitwise xor m n = m.xor n
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !xor x !y) m n = Nat.bitwise xor m n
<VAR>m n : ℕ<GOAL>Nat.bitwise (fun x y => !xor (!x) y) m n = Nat.bitwise xor m n
<VAR>m n : ℕ<GOAL>↑(Nat.bitwise (fun x y => xor (!x) !y) m n) = ↑(Nat.bitwise xor m n)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>T : Monad C<VAR>X Y Z : Kleisli T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>T.map (f ≫ T.map g ≫ T.μ.app Z) ≫ T.μ.app Z = { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ T.μ.app Y }.map f ≫ { obj := fun X => T.obj X, map := fun {x Y} f => T.map f ≫ T.μ.app Y }.map g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>T : Monad C<VAR>X Y Z : Kleisli T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>T.map f ≫ T.map (T.map g) ≫ T.map (T.μ.app Z) ≫ T.μ.app Z = T.map f ≫ T.μ.app Y ≫ T.map g ≫ T.μ.app Z
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>T : Monad C<VAR>X Y Z : Kleisli T<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>T.map f ≫ T.map (T.map g) ≫ T.μ.app (T.obj Z) ≫ T.μ.app Z = T.map f ≫ (T.toFunctor ⋙ T.toFunctor).map g ≫ T.μ.app (T.obj Z) ≫ T.μ.app Z