ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G<VAR>hg'invf : φ.leftDeriv.comp g'inv = 0<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)<GOAL>HasStrictFDerivAt (φ.implicitFunction (φ.leftFun φ.pt)) g'inv (φ.rightFun φ.pt)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>hg'inv : φ.rightDeriv.comp g'inv = ContinuousLinearMap.id 𝕜 G<VAR>hg'invf : φ.leftDeriv.comp g'inv = 0<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)<GOAL>g'inv = (↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm).comp (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G))
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)<VAR>hg'inv : ∀ (x : G), φ.rightDeriv (g'inv x) = (ContinuousLinearMap.id 𝕜 G) x<VAR>hg'invf : ∀ (x : G), φ.leftDeriv (g'inv x) = 0 x<GOAL>∀ (x : G), g'inv x = ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm ((ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)<VAR>hg'inv : ∀ (x : G), φ.rightDeriv (g'inv x) = (ContinuousLinearMap.id 𝕜 G) x<VAR>hg'invf : ∀ (x : G), φ.leftDeriv (g'inv x) = 0 x<VAR>x : G<GOAL>g'inv x = ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm ((ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : CompleteSpace F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace G<VAR>φ : ImplicitFunctionData 𝕜 E F G<VAR>g'inv : G →L[𝕜] E<VAR>this : HasStrictFDerivAt (HasStrictFDerivAt.localInverse φ.prodFun (φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) φ.pt ⋯) ↑(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯).symm (φ.leftFun φ.pt, φ.rightFun φ.pt)<VAR>hg'inv : ∀ (x : G), φ.rightDeriv (g'inv x) = (ContinuousLinearMap.id 𝕜 G) x<VAR>hg'invf : ∀ (x : G), φ.leftDeriv (g'inv x) = 0 x<VAR>x : G<GOAL>(φ.leftDeriv.equivProdOfSurjectiveOfIsCompl φ.rightDeriv ⋯ ⋯ ⋯) (g'inv x) = (ContinuousLinearMap.prod 0 (ContinuousLinearMap.id 𝕜 G)) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Monoid α<VAR>s t : Set α<VAR>a : α<VAR>m n✝ n : ℕ<VAR>x✝ : n + 2 ≠ 0<GOAL>univ ^ (n + 2) = univ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y : C<GOAL>((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫ ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom = 𝟙 (tensorObj ℬ X Y)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y : C<GOAL>∀ (j : Discrete WalkingPair), (((ℬ X Y).isLimit.conePointUniqueUpToIso (ℬ Y X).isLimit.swapBinaryFan).hom ≫ ((ℬ Y X).isLimit.conePointUniqueUpToIso (ℬ X Y).isLimit.swapBinaryFan).hom) ≫ (ℬ X Y).cone.π.app j = 𝟙 (tensorObj ℬ X Y) ≫ (ℬ X Y).cone.π.app j
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<VAR>b : β<GOAL>b ∈ pmap f l H ↔ ∃ a h, f a ⋯ = b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>span {(mk W) (C (X - C (W.addX x₁ x₂ L))), (mk W) (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)))} = span {(mk W) (-Y - C (C W.a₁ * X + C W.a₃) - C (C L * (X - C x₁) + C y₁))} ⊔ span {(mk W) (C (X - C (W.addX x₁ x₂ L)))}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>span {(mk W) (C (X - C (W.addX x₁ x₂ L))), (mk W) (Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) + C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)))} = span {(mk W) (C (X - C (W.addX x₁ x₂ L))), (mk W) (C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y)}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>Y - C (C (-(L * (W.addX x₁ x₂ L - x₁) + y₁) - W.a₁ * W.addX x₁ x₂ L - W.a₃)) + C (X - C (W.addX x₁ x₂ L)) * C (C (W.a₁ + L)) = C (C W.a₁ * X + C W.a₃) + C (C L * (X - C x₁) + C y₁) + Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x₁ x₂ y₁ L : R<GOAL>Y - (-(C (C L) * (C (C (W.addX x₁ x₂ L)) - C (C x₁)) + C (C y₁)) - C (C W.a₁) * C (C (W.addX x₁ x₂ L)) - C (C W.a₃)) + (C X - C (C (W.addX x₁ x₂ L))) * (C (C W.a₁) + C (C L)) = C (C W.a₁) * C X + C (C W.a₃) + (C (C L) * (C X - C (C x₁)) + C (C y₁)) + Y
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<GOAL>∃ q a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<GOAL>∃ q a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<VAR>hle : ↑n ≤ ↑m<GOAL>∃ q a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<VAR>hle : ↑n ≤ ↑m<VAR>hm : ↑m ≤ Fintype.card σ<GOAL>∃ q a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<VAR>hle : ↑n ≤ ↑m<VAR>hm : ↑m ≤ Fintype.card σ<GOAL>M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) = M.evalFrom s (List.take (↑n) (List.take (↑m) x)) ∧ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<VAR>hle : ↑n ≤ ↑m<VAR>hm : ↑m ≤ Fintype.card σ<VAR>hq : M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) = M.evalFrom s (List.take (↑n) (List.take (↑m) x))<GOAL>M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) = M.evalFrom s (List.take (↑n) (List.take (↑m) x)) ∧ M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>inst✝ : Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<VAR>n m : Fin (Fintype.card σ + 1)<VAR>hneq : n ≠ m<VAR>heq : M.evalFrom s (List.take (↑n) x) = M.evalFrom s (List.take (↑m) x)<VAR>hle : ↑n ≤ ↑m<VAR>hm : ↑m ≤ Fintype.card σ<VAR>hq : M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑n) (List.take (↑m) x)) = M.evalFrom s (List.take (↑n) (List.take (↑m) x))<GOAL>M.evalFrom (M.evalFrom s (List.take (↑n) (List.take (↑m) x))) (List.drop (↑m) x) = t
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>M : Matrix V V α<VAR>v w : V<GOAL>(M * adjMatrix α G) v w = ∑ u ∈ G.neighborFinset w, M v u
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℤ<VAR>hn : n < 0<GOAL>Tendsto (fun x => x ^ n) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℤ<VAR>hn : n < 0<VAR>N : ℕ<VAR>h : ↑N = -n<GOAL>Tendsto (fun x => x ^ n) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>n : ℤ<VAR>N : ℕ<VAR>hn : 0 < N<VAR>h : ↑N = -n<GOAL>Tendsto (fun x => x ^ n) atTop (𝓝 0)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X Y Z : Dial C<GOAL>((X.tensorObj Y).tensorObj Z).rel = (Subobject.pullback (prod.map (prod.associator X.src Y.src Z.src).hom (prod.associator X.tgt Y.tgt Z.tgt).hom)).obj (X.tensorObj (Y.tensorObj Z)).rel
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>S ∈ leftTransversals T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g) ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>‖⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>∀ᵐ (x : α) ∂μ, ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<GOAL>∀ (x : α), ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x → ‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<VAR>x : α<VAR>hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x<GOAL>‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖₊ ≤ ‖f‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : SecondCountableTopologyEither α E<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : α →ᵇ E<VAR>x : α<VAR>hx : ↑(ContinuousMap.toAEEqFun μ f.toContinuousMap) x = f.toContinuousMap x<GOAL>‖↑↑⟨ContinuousMap.toAEEqFun μ f.toContinuousMap, ⋯⟩ x‖ ≤ ‖f‖
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>S : Set (Set α)<VAR>hK : IsCompact K<VAR>hopen : ∀ s ∈ S, IsOpen s<VAR>hcover : K ⊆ ⋃₀ S<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>K : Set α<VAR>S : Set (Set α)<VAR>hK : IsCompact K<VAR>hopen : ∀ s ∈ S, IsOpen s<VAR>hcover : K ⊆ ⋃ i, ↑i<GOAL>∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>k : ℕ<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors<VAR>a✝ : Nontrivial α<GOAL>∃ b, a = b ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count (Associates.mk a0).factors<GOAL>∃ b, Associates.mk a0 = b ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<GOAL>∃ b, Associates.mk a0 = b ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<VAR>hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)<GOAL>∃ b, Associates.mk a0 = b ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<VAR>hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)<VAR>u : Multiset { a // Irreducible a }<VAR>hu : factors' a0 = k • u<GOAL>∃ b, Associates.mk a0 = b ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<VAR>hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)<VAR>u : Multiset { a // Irreducible a }<VAR>hu : factors' a0 = k • u<GOAL>Associates.mk a0 = FactorSet.prod ↑u ^ k
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<VAR>hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)<VAR>u : Multiset { a // Irreducible a }<VAR>hu : factors' a0 = k • u<GOAL>(Associates.mk a0).factors = (FactorSet.prod ↑u ^ k).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>k : ℕ<VAR>a✝ : Nontrivial α<VAR>a0 : α<VAR>hz : a0 ≠ 0<VAR>ha : Associates.mk a0 ≠ 0<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count ↑(factors' a0)<VAR>hk' : ∀ p ∈ factors' a0, k ∣ Multiset.count p (factors' a0)<VAR>u : Multiset { a // Irreducible a }<VAR>hu : factors' a0 = k • u<GOAL>↑(k • u) = k • ↑u
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A : Type u_2<VAR>inst✝² : AddGroup A<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>inst✝¹ : (i : η) → Group (f i)<VAR>inst✝ : DecidableEq η<VAR>I : Finset η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h1 : ∀ i ∉ I, x i = 1<VAR>h2 : ∀ i ∈ I, Pi.mulSingle i (x i) ∈ H<GOAL>x ∈ H
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A : Type u_2<VAR>inst✝² : AddGroup A<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>inst✝¹ : (i : η) → Group (f i)<VAR>inst✝ : DecidableEq η<VAR>H : Subgroup ((i : η) → f i)<VAR>x : (i : η) → f i<VAR>h1 : ∀ i ∉ ∅, x i = 1<VAR>h2 : ∀ i ∈ ∅, Pi.mulSingle i (x i) ∈ H<GOAL>x ∈ H
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A : Type u_2<VAR>inst✝² : AddGroup A<VAR>η : Type u_3<VAR>f : η → Type u_4<VAR>inst✝¹ : (i : η) → Group (f i)<VAR>inst✝ : DecidableEq η<VAR>H : Subgroup ((i : η) → f i)<VAR>i : η<VAR>I : Finset η<VAR>hnmem : i ∉ I<VAR>ih : ∀ (x : (i : η) → f i), (∀ i ∉ I, x i = 1) → (∀ i ∈ I, Pi.mulSingle i (x i) ∈ H) → x ∈ H<VAR>x : (i : η) → f i<VAR>h1 : ∀ i_1 ∉ insert i I, x i_1 = 1<VAR>h2 : ∀ i_1 ∈ insert i I, Pi.mulSingle i_1 (x i_1) ∈ H<GOAL>x ∈ H
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<GOAL>constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>inj : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>constantCoeff (wittStructureInt p Φ 0) = constantCoeff Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>inj : Function.Injective ⇑(Int.castRingHom ℚ)<GOAL>(Int.castRingHom ℚ) (constantCoeff (wittStructureInt p Φ 0)) = (Int.castRingHom ℚ) (constantCoeff Φ)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = h.h₂ ≫ S₂.g + h.h₃ + φ₂.τ₃
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂ + φ₂.τ₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.177771, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁✝ S₂✝ S₃ : ShortComplex C<VAR>φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>φ₁ φ₂ : S₁ ⟶ S₂<VAR>h : Homotopy φ₁ φ₂<GOAL>S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v w : Fin 3 → R<GOAL>v ⬝ᵥ (crossProduct v) w = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>v w : Fin 3 → R<GOAL>v 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 + v 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 + v 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : IsDedekindDomain B<VAR>I J : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>hJ : J ≠ 0<VAR>hIJ : I * J ≤ 1<GOAL>J ≤ dual A K I