ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>inst✝² : Groupoid G<VAR>inst✝¹ : IsFreeGroupoid G<VAR>T : WideSubquiver (Symmetrify (Generators G))<VAR>inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)<VAR>a : G<VAR>p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a<GOAL>treeHom T a = homOfPath T p
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<GOAL>|o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this : FiniteDimensional ℝ E<GOAL>|o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<GOAL>|o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<GOAL>|o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>|o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>∏ x : Fin n.succ, |⟪b x, v x⟫_ℝ| ≤ ∏ i : Fin (n + 1), ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>∀ i ∈ Finset.univ, 0 ≤ |⟪b i, v i⟫_ℝ|
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<GOAL>∀ i ∈ Finset.univ, |⟪b i, v i⟫_ℝ| ≤ ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>i : Fin n.succ<VAR>a✝ : i ∈ Finset.univ<GOAL>|⟪b i, v i⟫_ℝ| ≤ ‖v i‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>v : Fin (n + 1) → E<VAR>this✝ : FiniteDimensional ℝ E<VAR>this : finrank ℝ E = Fintype.card (Fin n.succ)<VAR>b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v<VAR>hb : b.toBasis.det v = ∏ i : Fin n.succ, ⟪b i, v i⟫_ℝ<VAR>i : Fin n.succ<VAR>a✝ : i ∈ Finset.univ<GOAL>‖v i‖ = ‖b i‖ * ‖v i‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>(∀ᵐ (x : α) ∂μ, x ∉ s) ↔ μ s = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F : Presheaf C X<VAR>x : ↑X<VAR>t : (forget C).obj (F.stalk x)<GOAL>∃ U, ∃ (m : x ∈ U), ∃ s, (F.germ ⟨x, m⟩) s = t
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesFilteredColimits (forget C)<VAR>F : Presheaf C X<VAR>x : ↑X<VAR>t : (forget C).obj (F.stalk x)<VAR>U : (OpenNhds x)ᵒᵖ<VAR>s : (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F ⋙ forget C).obj U<VAR>e : ((forget C).mapCocone (colimit.cocone (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F))).ι.app U s = t<GOAL>∃ U, ∃ (m : x ∈ U), ∃ s, (F.germ ⟨x, m⟩) s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : DecidableEq β<VAR>f g : α →. β<VAR>inst✝¹ : (x : α) → Decidable (f x).Dom<VAR>inst✝ : (x : α) → Decidable (g x).Dom<VAR>s t✝ : Finset α<VAR>b : β<VAR>t : Finset β<GOAL>pimage f s ⊆ t ↔ ∀ x ∈ s, ∀ y ∈ f x, y ∈ t
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>σ : ι → Type u_7<VAR>τ : κ → Type u_8<VAR>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f : Sigma σ → X<GOAL>IsOpenMap f ↔ ∀ (i : ι), IsOpenMap fun a => f ⟨i, a⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<VAR>this : ∀ (x y : P.M α), EqvGen R x y → x = y<GOAL>x = y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>Equivalence (EqvGen R)
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → (TypeVec.id ::: Quot.mk R) <$$> dest P x = (TypeVec.id ::: Quot.mk R) <$$> dest P y<VAR>x y : P.M α<VAR>r : R x y<GOAL>∀ (x y : P.M α), EqvGen R x y → (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P x = (TypeVec.id ::: Quot.mk (EqvGen R)) <$$> dest P y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<GOAL>LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>h : Codisjoint (rootSpace H 0) (LieModule.posFittingComp R (↥H) L)<GOAL>LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>h : Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)<GOAL>LinearMap.ker ((killingForm R L).restrict H.toSubmodule) = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>h : Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)<GOAL>∀ m₀ ∈ H, ∀ m₁ ∈ LieModule.posFittingComp R (↥H) L, ((killingForm R L) m₀) m₁ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : IsKilling R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : Module.Free R L<VAR>inst✝² : IsNoetherian R L<VAR>inst✝¹ : IsArtinian R L<VAR>H : LieSubalgebra R L<VAR>inst✝ : H.IsCartanSubalgebra<VAR>h : Codisjoint H.toSubmodule ↑(LieModule.posFittingComp R (↥H) L)<VAR>m₀ : L<VAR>h₀ : m₀ ∈ H<VAR>m₁ : L<VAR>h₁ : m₁ ∈ LieModule.posFittingComp R (↥H) L<GOAL>((killingForm R L) m₀) m₁ = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>x y : Associates ↥R⁰<GOAL>↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) = ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) x) * ↑↑((associatesNonZeroDivisorsEquivIsPrincipal R) y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ + ν₁ = μ + ν₂<GOAL>ν₁ = ν₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ + ν₁ = μ + ν₂<GOAL>∀ (i : ℕ), ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s✝ t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ + ν₁ = μ + ν₂<VAR>i : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ν₁.restrict (spanningSets μ i)) s = (ν₂.restrict (spanningSets μ i)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s✝ t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>h : μ + ν₁ = μ + ν₂<VAR>i : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s = μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν ν₁✝ ν₂✝ : Measure α<VAR>s✝ t : Set α<VAR>μ ν₁ ν₂ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>i : ℕ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>h : ∀ (s : Set α), μ s + ν₁ s = μ s + ν₂ s<GOAL>μ (s ∩ spanningSets μ i) + (ν₁.restrict (spanningSets μ i)) s = μ (s ∩ spanningSets μ i) + (ν₂.restrict (spanningSets μ i)) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableRel Disjoint<VAR>s t u v : Finset α<GOAL>s ○ t ○ u = s ○ u ○ t
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>b : ι → M<VAR>n : ℕ<VAR>N : Submodule R M<VAR>snf : SmithNormalForm N ι n<VAR>m✝ : ↥N<VAR>i : Fin n<VAR>m : ↥N<GOAL>(snf.bM.coord (snf.f i) ∘ₗ N.subtype) m = (snf.a i • snf.bN.coord i) m
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>f g : ℕ → R<VAR>n : ℕ<GOAL>((fun x => χ ↑x) * f ⍟ ((fun x => χ ↑x) * g)) n = ((fun x => χ ↑x) * (f ⍟ g)) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>f g : ℕ → R<VAR>n : ℕ<GOAL>∑ x ∈ n.divisorsAntidiagonal, χ ↑x.1 * f x.1 * (χ ↑x.2 * g x.2) = ∑ i ∈ n.divisorsAntidiagonal, χ ↑n * (f i.1 * g i.2)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>f g : ℕ → R<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑n * (f p.1 * g p.2)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>n✝ : ℕ<VAR>χ : DirichletCharacter R n✝<VAR>f g : ℕ → R<VAR>n : ℕ<VAR>p : ℕ × ℕ<VAR>hp : p ∈ n.divisorsAntidiagonal<GOAL>χ ↑p.1 * f p.1 * (χ ↑p.2 * g p.2) = χ ↑p.1 * χ ↑p.2 * (f p.1 * g p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f g : Ultrafilter α<VAR>s t : Set α<VAR>p q : α → Prop<VAR>m : α → β<VAR>a : α<VAR>inj : Injective m<VAR>large : range m ∈ pure (m a)<GOAL>𝓟 (m ⁻¹' {m a}) = ↑(pure a)
<VAR>x : ℂ<VAR>h : x.arg ≠ π<GOAL>log ((starRingEnd ℂ) x) = (starRingEnd ℂ) (log x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>inst✝ : Semiring T<VAR>p : T[X]<VAR>g : ℕ → T → R[X]<VAR>x : S<GOAL>eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)
<VAR>R : Type u<VAR>S : Type v<VAR>T✝ : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>inst✝ : Semiring T✝<VAR>p : T✝[X]<VAR>g : ℕ → T✝ → R[X]<VAR>x : S<VAR>T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }<GOAL>eval₂ f x (p.sum g) = p.sum fun n a => eval₂ f x (g n a)
<VAR>R : Type u<VAR>S : Type v<VAR>T✝ : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x✝ : S<VAR>inst✝ : Semiring T✝<VAR>p : T✝[X]<VAR>g : ℕ → T✝ → R[X]<VAR>x : S<VAR>T : R[X] →+ S := { toFun := eval₂ f x, map_zero' := ⋯, map_add' := ⋯ }<VAR>A : ∀ (y : R[X]), eval₂ f x y = T y<GOAL>T (p.sum g) = p.sum fun n a => T (g n a)
<VAR>n : ℕ<GOAL>χ₄ ↑n = χ₄ ↑(n % 4)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>∀ (x : ExteriorAlgebra R M), x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : ExteriorAlgebra R M<GOAL>x ∈ Submodule.span R (Set.range fun x => (ιMulti R x.fst) x.snd)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsPreorder α r<VAR>h : s.PartiallyWellOrderedOn r<GOAL>s.WellFoundedOn fun a b => r a b ∧ ¬r b a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsPreorder α r<VAR>h : s.PartiallyWellOrderedOn r<VAR>this : Preorder α := Preorder.mk ⋯ ⋯ ⋯<GOAL>s.WellFoundedOn fun a b => r a b ∧ ¬r b a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsPreorder α r<VAR>this : Preorder α := Preorder.mk ⋯ ⋯ ⋯<VAR>h : s.PartiallyWellOrderedOn fun x x_1 => x ≤ x_1<GOAL>s.WellFoundedOn fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsPreorder α r<VAR>this : Preorder α := Preorder.mk ⋯ ⋯ ⋯<VAR>h : s.PartiallyWellOrderedOn fun x x_1 => x ≤ x_1<GOAL>∀ (f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1), ¬∀ (n : ℕ), f n ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t : Set α<VAR>a : α<VAR>inst✝ : IsPreorder α r<VAR>this : Preorder α := Preorder.mk ⋯ ⋯ ⋯<VAR>h : s.PartiallyWellOrderedOn fun x x_1 => x ≤ x_1<VAR>f : (fun x x_1 => x > x_1) ↪r fun x x_1 => x < x_1<VAR>hf : ∀ (n : ℕ), f n ∈ s<VAR>m n : ℕ<VAR>hlt : m < n<VAR>hle : f m ≤ f n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Mul α<VAR>i : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝ : PartialOrder α<VAR>a : α<VAR>ha : MulLECancellable a<VAR>b c : α<VAR>h : (fun x => x * a) b = (fun x => x * a) c<GOAL>a * b = a * c
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => (fourier n) ↑y) (2 * ↑π * I * ↑n / ↑T * (fourier n) ↑x) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * ↑y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (2 * ↑π * I * ↑n / ↑T * cexp (2 * ↑π * I * ↑n * ↑x / ↑T)) ↑x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => cexp (2 * ↑π * I * ↑n * y / ↑T)) (cexp (2 * ↑π * I * ↑n * ↑x / ↑T) * (2 * ↑π * I * ↑n / ↑T)) ↑x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>HasDerivAt (fun y => 2 * ↑π * I * ↑n * y / ↑T) (2 * ↑π * I * ↑n / ↑T) ↑x
<VAR>T : ℝ<VAR>n : ℤ<VAR>x : ℝ<GOAL>(fun y => 2 * ↑π * I * ↑n * y / ↑T) = fun x => x * (2 * ↑π * I * ↑n / ↑T)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.318794, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 4<VAR>app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯<VAR>app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯<VAR>w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯<GOAL>3 < 4 + 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<GOAL>normEDS b c d 0 = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>hK : K ≠ ⊤<GOAL>1 ∉ comap f K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<VAR>K L : Ideal S<VAR>hK : K ≠ ⊤<GOAL>1 ∉ K
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>x₁ x₂ : α<GOAL>edist ((WithLp.equiv p (α × β)).symm (x₁, 0)) ((WithLp.equiv p (α × β)).symm (x₂, 0)) = edist x₁ x₂
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>h : IsOpen t<GOAL>closure s ∩ t ⊆ closure (s ∩ t)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : SizeOf α<VAR>x : α<VAR>s : Multiset α<VAR>hx : x ∈ s<GOAL>sizeOf x < sizeOf s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : SizeOf α<VAR>x : α<VAR>l : List α<VAR>hx : x ∈ Quot.mk Setoid.r l<GOAL>sizeOf x < sizeOf (Quot.mk Setoid.r l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>preimage Eq s = s
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<GOAL>(∃ r, 0 ≤ r ∧ r • x = y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>hx : x ≠ 0<VAR>h : ∃ r, 0 ≤ r ∧ r • x = y<GOAL>SameRay R x y
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>r : R<VAR>hr : 0 ≤ r<GOAL>SameRay R x (r • x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<GOAL>((StrictMono fun a => map f ↑a) ∧ ∀ (x : α), map f ↑x < map f ⊤) ↔ StrictMono f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹² : RCLike 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup F'<VAR>inst✝⁸ : NormedSpace 𝕜 F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : CompleteSpace F'<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedAddCommGroup G'<VAR>inst✝³ : NormedSpace ℝ G'<VAR>inst✝² : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝¹ : NormedSpace ℝ G<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>x : G<GOAL>(condexpInd G hm μ (s ∪ t)) x = (⇑(condexpInd G hm μ s) + ⇑(condexpInd G hm μ t)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(condDistrib Y X μ) x) (Measure.map X μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x) (Measure.map (fun a => (X a, Y a)) μ).fst
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<GOAL>(q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<GOAL>(q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den
<VAR>q r : ℚ<VAR>s : ℚ := (q.num * ↑r.den + r.num * ↑q.den) /. (↑q.den * ↑r.den)<VAR>hs : ↑q.den * ↑r.den ≠ 0<VAR>c : ℤ<VAR>c_mul_num : q.num * ↑r.den + r.num * ↑q.den = c * (↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).num<VAR>c_mul_den : ↑q.den * ↑r.den = c * ↑(↑(q.num * ↑r.den + r.num * ↑q.den) / ↑(↑q.den * ↑r.den)).den<GOAL>(q + r).num * ↑q.den * ↑r.den = (q.num * ↑r.den + r.num * ↑q.den) * ↑(q + r).den