ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<VAR>j : τ<VAR>h : j ∈ ((rename f) φ).vars<GOAL>∃ i ∈ φ.vars, f i = j
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r✝ : α → α → Prop<VAR>a b : α<VAR>r : α → β → Prop<VAR>hr : Relator.BiUnique r<GOAL>(fun x x_1 => x ↔ x_1) [].Nodup [].Nodup
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁ l₂ : List α<VAR>r✝ : α → α → Prop<VAR>a b : α<VAR>r : α → β → Prop<VAR>hr : Relator.BiUnique r<VAR>a✝ : α<VAR>b✝ : β<VAR>l₁✝ : List α<VAR>l₂✝ : List β<VAR>hab : r a✝ b✝<VAR>h : Forall₂ r l₁✝ l₂✝<GOAL>(fun x x_1 => x ↔ x_1) (a✝ :: l₁✝).Nodup (b✝ :: l₂✝).Nodup
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).join = l<VAR>l : List α<VAR>h : n + ns.sum = l.length<GOAL>(l.splitWrtCompositionAux (n :: ns)).join = l
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>ns : List ℕ<VAR>IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).join = l<VAR>l : List α<VAR>h : n + ns.sum = l.length<GOAL>(take n l :: (drop n l).splitWrtCompositionAux ns).join = l
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>(X ^ n).natTrailingDegree = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>p q : Multiset α<GOAL>Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>p q : Multiset α<GOAL>Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<GOAL>f = f ⇑e • e.det
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>i : ι → ι<VAR>h : Injective i<GOAL>(f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>i : ι → ι<VAR>h : Injective i<VAR>σ : Equiv.Perm ι := Equiv.ofBijective i ⋯<GOAL>(f fun i_1 => e (i i_1)) = (f ⇑e • e.det) fun i_1 => e (i i_1)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>e : Basis ι R M<VAR>f : M [⋀^ι]→ₗ[R] R<VAR>i : ι → ι<VAR>h : Injective i<VAR>σ : Equiv.Perm ι := Equiv.ofBijective i ⋯<GOAL>f (⇑e ∘ ⇑σ) = (f ⇑e • e.det) (⇑e ∘ ⇑σ)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>E' : Type u_3<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<GOAL>ContDiff 𝕜 n (Prod.map f g)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>E' : Type u_3<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>F' : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace 𝕜 F'<VAR>f : E → F<VAR>g : E' → F'<VAR>hf : ∀ (x : E), ContDiffAt 𝕜 n f x<VAR>hg : ∀ (x : E'), ContDiffAt 𝕜 n g x<GOAL>∀ (x : E × E'), ContDiffAt 𝕜 n (Prod.map f g) x
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K H : Subgroup G<GOAL>↑H = ↑⊤ ↔ ↑H = Set.univ
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>toOpen ↑(Γ.obj (op X)) ⊤ ≫ X.toΓSpec.val.c.app (op ⊤) = 𝟙 (Γ.obj (op X))
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ (structureSheaf ↑(Γ.obj (op X))).val.map (eqToHom ⋯).op) ≫ X.toΓSpec.val.c.app (op ⊤) = 𝟙 (Γ.obj (op X))
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ (structureSheaf ↑(Γ.obj (op X))).val.map (eqToHom ⋯).op ≫ X.toΓSpec.val.c.app (op ⊤) = 𝟙 (Γ.obj (op X))
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>(toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ X.toΓSpec.val.c.app (op (basicOpen 1))) ≫ ((pushforward CommRingCat X.toΓSpec.val.base).obj X.presheaf).map (eqToHom ⋯).op = 𝟙 (Γ.obj (op X))
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>X.presheaf.map ((X.toΓSpecMapBasicOpen 1).leTop.op ≫ (Opens.map X.toΓSpec.val.base).op.map (eqToHom ⋯).op) = 𝟙 (Γ.obj (op X))
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>op ⊤ = (Opens.map X.toΓSpec.val.base).op.obj (op ⊤)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>π : α → Type u_6<VAR>inst✝¹ : (x : α) → CommMonoid (π x)<VAR>inst✝ : (x : α) → TopologicalSpace (π x)<VAR>f : ι → (x : α) → π x<GOAL>Multipliable f ↔ ∀ (x : α), Multipliable fun i => f i x
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<GOAL>(fun x => (algebraMap R C) x.fst + φ x.snd) 1 = 1
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯ }.toFun ((inl x_r + ↑x_a) * (inl y_r + ↑y_a)) = { toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯ }.toFun (inl x_r + ↑x_a) * { toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯ }.toFun (inl y_r + ↑y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>(algebraMap R C) x_r * (algebraMap R C) y_r + (x_r • φ y_a + y_r • φ x_a + φ x_a * φ y_a) = ((algebraMap R C) x_r + φ x_a) * ((algebraMap R C) y_r + φ y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>(algebraMap R C) x_r * (algebraMap R C) y_r + (x_r • φ y_a + y_r • φ x_a + φ x_a * φ y_a) = (algebraMap R C) x_r * (algebraMap R C) y_r + (algebraMap R C) x_r * φ y_a + (φ x_a * (algebraMap R C) y_r + φ x_a * φ y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>(algebraMap R C) x_r * (algebraMap R C) y_r + (x_r • φ y_a + y_r • φ x_a + φ x_a * φ y_a) = (algebraMap R C) x_r * (algebraMap R C) y_r + (algebraMap R C) x_r * φ y_a + ((algebraMap R C) y_r * φ x_a + φ x_a * φ y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<GOAL>(↑{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯ }).toFun 0 = 0
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>(↑{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯ }).toFun (inl x_r + ↑x_a + (inl y_r + ↑y_a)) = (↑{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯ }).toFun (inl x_r + ↑x_a) + (↑{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯ }).toFun (inl y_r + ↑y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>x_r : R<VAR>x_a : A<VAR>y_r : R<VAR>y_a : A<GOAL>(algebraMap R C) x_r + (algebraMap R C) y_r + (φ x_a + φ y_a) = (algebraMap R C) x_r + φ x_a + ((algebraMap R C) y_r + φ y_a)
<VAR>S : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝¹² : CommSemiring S<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : NonUnitalSemiring A<VAR>inst✝⁹ : Module R A<VAR>inst✝⁸ : SMulCommClass R A A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>B : Type u_4<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : Algebra S B<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : DistribMulAction S A<VAR>inst✝² : IsScalarTower S R A<VAR>C : Type u_5<VAR>inst✝¹ : Semiring C<VAR>inst✝ : Algebra R C<VAR>φ : A →ₙₐ[R] C<VAR>r : R<GOAL>(↑↑{ toFun := fun x => (algebraMap R C) x.fst + φ x.snd, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }).toFun ((algebraMap R (Unitization R A)) r) = (algebraMap R C) r
<VAR>xl✝ xr✝ xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>(-mk yl yr yL yR ≤ -mk xl xr xL xR ↔ mk xl xr xL xR ≤ mk yl yr yL yR) ∧ (-mk yl yr yL yR ⧏ -mk xl xr xL xR ↔ mk xl xr xL xR ⧏ mk yl yr yL yR)
<VAR>xl✝ xr✝ xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u<VAR>yL : yl → PGame<VAR>yR : yr → PGame<GOAL>(((∀ (i : yr), -yR i ⧏ -mk xl xr xL xR) ∧ ∀ (j : xl), -mk yl yr yL yR ⧏ -xL j) ↔ (∀ (i : xl), xL i ⧏ mk yl yr yL yR) ∧ ∀ (j : yr), mk xl xr xL xR ⧏ yR j) ∧ (((∃ i, -mk yl yr yL yR ≤ -xR i) ∨ ∃ j, -yL j ≤ -mk xl xr xL xR) ↔ (∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>γ : Path x y<VAR>a₁ a₂ a₃ : X<VAR>b₁ b₂ b₃ : Y<VAR>γ₁ : Path a₁ a₂<VAR>δ₁ : Path a₂ a₃<VAR>γ₂ : Path b₁ b₂<VAR>δ₂ : Path b₂ b₃<GOAL>(γ₁.prod γ₂).trans (δ₁.prod δ₂) = (γ₁.trans δ₁).prod (γ₂.trans δ₂)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>π : ι → Set (Set Ω)<VAR>a : ι<VAR>S : Finset ι<VAR>hp_ind : iIndepSets π κ μ<VAR>haS : a ∉ S<VAR>t1 t2 : Set Ω<VAR>s : Finset ι<VAR>hs_mem : ↑s ⊆ ↑S<VAR>ft1 : ι → Set Ω<VAR>hft1_mem : ∀ x ∈ s, ft1 x ∈ π x<VAR>ht1_eq : t1 = ⋂ x ∈ s, ft1 x<VAR>ht2_mem_pia : t2 ∈ π a<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>π : ι → Set (Set Ω)<VAR>a : ι<VAR>S : Finset ι<VAR>hp_ind : iIndepSets π κ μ<VAR>haS : a ∉ S<VAR>t1 t2 : Set Ω<VAR>s : Finset ι<VAR>hs_mem : s ⊆ S<VAR>ft1 : ι → Set Ω<VAR>hft1_mem : ∀ x ∈ s, ft1 x ∈ π x<VAR>ht1_eq : t1 = ⋂ x ∈ s, ft1 x<VAR>ht2_mem_pia : t2 ∈ π a<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<GOAL>0⁻¹ = 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>ht : Subsingleton α<GOAL>0⁻¹ = 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>ht : Nontrivial α<GOAL>0⁻¹ = 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>ht : Nontrivial α<VAR>hc : 0 = Fintype.card n<GOAL>0⁻¹ = 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>ht : Nontrivial α<VAR>hc : 0 < Fintype.card n<GOAL>0⁻¹ = 0
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>map (𝟙 Y) = 𝟭 (Over Y)
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>∀ (X : Over Y), (map (𝟙 Y)).obj X = (𝟭 (Over Y)).obj X
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X Y : T<GOAL>autoParam (∀ (X Y_1 : Over Y) (f : X ⟶ Y_1), (map (𝟙 Y)).map f = eqToHom ⋯ ≫ (𝟭 (Over Y)).map f ≫ eqToHom ⋯) _auto✝
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌈0⌉₊ = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>(p * q) (ap + aq) = p ap * q aq
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>(∑ x ∈ p.support, ∑ x_1 ∈ q.support, if x + x_1 = ap + aq then p x * q x_1 else 0) = p ap * q aq
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>∀ b ∈ q.support, b ≠ aq → (if ap + b = ap + aq then p ap * q b else 0) = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>aq ∉ q.support → (if ap + aq = ap + aq then p ap * q aq else 0) = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>∀ b ∈ p.support, b ≠ ap → (∑ x ∈ q.support, if b + x = ap + aq then p b * q x else 0) = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Ring R'<VAR>inst✝⁵ : AddZeroClass A<VAR>inst✝⁴ : SemilatticeSup B<VAR>inst✝³ : Add B<VAR>inst✝² : OrderBot B<VAR>D : A → B<VAR>p q : R[A]<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hD : Function.Injective D<VAR>ap aq : A<VAR>hp : supDegree D p ≤ D ap<VAR>hq : supDegree D q ≤ D aq<GOAL>ap ∉ p.support → (∑ x ∈ q.support, if ap + x = ap + aq then p ap * q x else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<GOAL>g (limsup u f) = limsup (fun x => g (u x)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<GOAL>limsup (fun x => g (u x)) f ≤ g (limsup u f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<GOAL>g (g.symm (limsup (fun x => g (u x)) f)) ≤ g (limsup u f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<GOAL>g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hf : u = fun i => g.symm (g (u i))<GOAL>g.symm (limsup (fun x => g (u x)) f) ≤ limsup u f