ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>ball x 0 = ∅
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>weightSpace M (α + ⇑(chainTop α β)) = ⊥
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>X₁ X₂ : Type v<VAR>M✝ N✝ M N : ModuleCat R<VAR>f : M ⟶ N<VAR>r : R<VAR>x : ↑((forget₂ (ModuleCat R) AddCommGrp).obj M)<GOAL>((forget₂ (ModuleCat R) AddCommGrp).map f ≫ N.smul r) x = (M.smul r ≫ (forget₂ (ModuleCat R) AddCommGrp).map f) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝ : OrderedRing 𝕜<VAR>f : ↑(stdSimplex 𝕜 (Fin 2))<GOAL>1 - ↑f 0 = ↑f 0 + ↑f 1 - ↑f 0
<VAR>ι : Type u<VAR>f : ι → Scheme<VAR>i : ι<GOAL>Sigma.ι f i ≫ (sigmaIsoGlued f).hom = (disjointGlueData f).ι i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>sublistsLen (n + 1) (a :: l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>sublistsLen (n + 1) l ++ map (id ∘ cons a) (sublistsLen n l) = sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l)
<VAR>n : PosNum<VAR>fuel : ℕ<VAR>ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1<VAR>k : PosNum<VAR>h : (↑n).sqrt < fuel + 1 + ↑k.bit1<GOAL>↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
<VAR>n : PosNum<VAR>fuel : ℕ<VAR>ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1<VAR>k : PosNum<VAR>h : (↑n).sqrt < fuel + 1 + ↑k.bit1<GOAL>↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) = if ↑n < ↑(k.bit1 * k.bit1) then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
<VAR>n : PosNum<VAR>fuel : ℕ<VAR>ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1<VAR>k : PosNum<VAR>h : (↑n).sqrt < fuel + 1 + ↑k.bit1<GOAL>↑(if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ) = if n < k.bit1 * k.bit1 then ↑n else if k.bit1 ∣ n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)
<VAR>n : PosNum<VAR>fuel : ℕ<VAR>ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1<VAR>k : PosNum<VAR>h : (↑n).sqrt < fuel + 1 + ↑k.bit1<VAR>h✝¹ : ¬n < k.bit1 * k.bit1<VAR>h✝ : ¬k.bit1 ∣ n<GOAL>↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<GOAL>dimH (f '' s) ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<GOAL>↑d ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : μH[↑d] (f '' s) ≤ ↑C ^ ↑d * μH[↑r * ↑d] s<GOAL>↑d ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤<GOAL>↑d ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤<VAR>Hrd : μH[↑(r * d)] s = ⊤<GOAL>↑d ≤ dimH s / ↑r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤<VAR>Hrd : μH[↑(r * d)] s = ⊤<GOAL>↑(r * d) ≤ dimH s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤<VAR>Hrd : μH[↑(r * d)] s = ⊤<GOAL>↑r ≠ 0 ∨ dimH s ≠ 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s t : Set X<VAR>h : HolderOnWith C r f s<VAR>hr : 0 < r<VAR>this✝³ : MeasurableSpace X := borel X<VAR>this✝² : BorelSpace X<VAR>this✝¹ : MeasurableSpace Y := borel Y<VAR>this✝ : BorelSpace Y<VAR>d : ℝ≥0<VAR>hd : μH[↑d] (f '' s) = ⊤<VAR>this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ⊤<VAR>Hrd : μH[↑(r * d)] s = ⊤<GOAL>↑r ≠ ⊤ ∨ dimH s ≠ ⊤
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) * y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y))) * orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>(orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)))).Coprime (orderOf (y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))))
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>(orderOf x).factorizationLCMLeft (orderOf y) * (orderOf x).factorizationLCMRight (orderOf y) = (orderOf x).lcm (orderOf y)
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>orderOf y ≠ 0
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>(orderOf x).factorizationLCMRight (orderOf y) ∣ orderOf y
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>orderOf x ≠ 0
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>(orderOf x).factorizationLCMLeft (orderOf y) ∣ orderOf x
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>x y : G<VAR>h : Commute x y<VAR>hx : orderOf x ≠ 0<VAR>hy : orderOf y ≠ 0<GOAL>((orderOf x).factorizationLCMLeft (orderOf y)).gcd ((orderOf x).factorizationLCMRight (orderOf y)) = 1
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>I : Ideal S<VAR>hI : I.IsMaximal<GOAL>(comap (algebraMap R S) I).IsMaximal
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>I : Ideal S<VAR>hI : I.IsMaximal<GOAL>IsField (R ⧸ comap (algebraMap R S) I)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>S : Type u_2<VAR>inst✝² : CommRing S<VAR>f : R →+* S<VAR>I✝ J : Ideal S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>I : Ideal S<VAR>hI : I.IsMaximal<VAR>this : (comap (algebraMap R S) I).IsPrime<GOAL>IsField (R ⧸ comap (algebraMap R S) I)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝³ : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubmonoidClass S M<VAR>A : ι → S<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(support fun i => ↑(x i)).Finite
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>p q : R[X]<VAR>x : R<VAR>inst✝ : CommSemiring S<VAR>f : R →+* S<GOAL>eval x (p.comp q) = eval (eval x q) p
<VAR>M : Type u_1<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝² : CommGroup G<VAR>g g' : G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasProd (fun n => f (n + k)) (g / ∏ i ∈ range k, f i) ↔ HasProd f g
<VAR>α : Type u_1<VAR>inst✝¹ : GroupWithZero α<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>Nat.card α = Nat.card αˣ + 1
<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>f : α → F<VAR>hq0_lt : 0 < q<VAR>hfq : eLpNorm' f q μ < ⊤<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ < ⊤
<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>f : α → F<VAR>hq0_lt : 0 < q<VAR>hfq : eLpNorm' f q μ < ⊤<GOAL>eLpNorm' f q μ ^ q < ⊤
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R✝ J I E R : Set α<GOAL>uniqueBaseOn I E ↾ R = uniqueBaseOn (I ∩ R ∩ E) R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I✝ X R✝ J I E R : Set α<GOAL>∀ I_1 ⊆ R, (I_1 ⊆ I ∧ I_1 ⊆ E) ∧ I_1 ⊆ R ↔ ((I_1 ⊆ I ∧ I_1 ⊆ R) ∧ I_1 ⊆ E) ∧ I_1 ⊆ R
<VAR>x✝ y x : ℝ<VAR>hx : cos x ≠ 0<GOAL>tan x * cos x = sin x
<VAR>a : ONote<VAR>ha : a.NF<VAR>b : ONote<VAR>hb : b.NF<GOAL>(a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩
<VAR>a : ONote<VAR>ha : a.NF<VAR>b : ONote<VAR>hb : b.NF<VAR>this : (a.cmp b).Compares a b<GOAL>(a.cmp b).Compares ⟨a, ha⟩ ⟨b, hb⟩
<VAR>a : ONote<VAR>ha : a.NF<VAR>b : ONote<VAR>hb : b.NF<VAR>h : a.cmp b = Ordering.eq<VAR>this : Ordering.eq.Compares a b<GOAL>Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>z : S<VAR>w w' v : P<GOAL>((toLocalizationWithZeroMap M S).lift g.toMonoidWithZeroHom hg) z * w + w' = v ↔ g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' = g ↑((toLocalizationMap M S).sec z).2 * v
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>g : R →+* P<VAR>hg : ∀ (y : ↥M), IsUnit (g ↑y)<VAR>z : S<VAR>w w' v : P<GOAL>↑g.toMonoidWithZeroHom ((toLocalizationWithZeroMap M S).sec z).1 * w + g ↑((toLocalizationWithZeroMap M S).sec z).2 * w' = g ↑((toLocalizationWithZeroMap M S).sec z).2 * v ↔ g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' = g ↑((toLocalizationMap M S).sec z).2 * v
<VAR>E : Type u_1<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup V<VAR>inst✝⁸ : InnerProductSpace ℝ V<VAR>inst✝⁷ : MeasurableSpace V<VAR>inst✝⁶ : BorelSpace V<VAR>inst✝⁵ : FiniteDimensional ℝ V<VAR>W : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : InnerProductSpace ℝ W<VAR>inst✝² : MeasurableSpace W<VAR>inst✝¹ : BorelSpace W<VAR>inst✝ : FiniteDimensional ℝ W<VAR>f : V → E<VAR>w : V<GOAL>𝓕 f w = ∫ (v : V), Complex.exp (↑(-2 * π * ⟪v, w⟫_ℝ) * Complex.I) • f v
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>v : V₁<GOAL>v ∈ f.ker ↔ f v = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : Integrable f μ<VAR>hν : Integrable f ν<GOAL>Integrable f (μ + ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : Memℒp f 1 μ<VAR>hν : Memℒp f 1 ν<GOAL>Memℒp f 1 (μ + ν)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : Memℒp f 1 μ<VAR>hν : Memℒp f 1 ν<GOAL>eLpNorm f 1 (μ + ν) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hμ : Memℒp f 1 μ<VAR>hν : Memℒp f 1 ν<GOAL>eLpNorm f 1 μ < ⊤ ∧ eLpNorm f 1 ν < ⊤
<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>r : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<GOAL>flip (r ∘r p) = flip p ∘r flip r
<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>r : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<VAR>c : γ<VAR>a : α<GOAL>flip (r ∘r p) c a = (flip p ∘r flip r) c a
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<GOAL>y ∈ I.splitCenterBox s ↔ y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<GOAL>(∀ (i : ι), y i ∈ Set.Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i) (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i)) ↔ ∀ (x : ι), y x ∈ Set.Ioc (I.lower x) (I.upper x) ∧ ((I.lower x + I.upper x) / 2 < y x ↔ x ∈ s)
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<VAR>i : ι<GOAL>y i ∈ Set.Ioc (s.piecewise (fun i => (I.lower i + I.upper i) / 2) I.lower i) (s.piecewise I.upper (fun i => (I.lower i + I.upper i) / 2) i) ↔ y i ∈ Set.Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<VAR>i : ι<GOAL>y i ∈ Set.Ioc (if i ∈ s then (I.lower i + I.upper i) / 2 else I.lower i) (if i ∈ s then I.upper i else (I.lower i + I.upper i) / 2) ↔ y i ∈ Set.Ioc (I.lower i) (I.upper i) ∧ ((I.lower i + I.upper i) / 2 < y i ↔ i ∈ s)
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<VAR>i : ι<VAR>hs : i ∈ s<GOAL>y i ∈ Set.Ioc ((I.lower i + I.upper i) / 2) (I.upper i) ↔ y i ∈ Set.Ioc (I.lower i) (I.upper i) ∧ (I.lower i + I.upper i) / 2 < y i
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>s : Set ι<VAR>y : ι → ℝ<VAR>i : ι<VAR>hs : i ∉ s<GOAL>y i ∈ Set.Ioc (I.lower i) ((I.lower i + I.upper i) / 2) ↔ y i ∈ Set.Ioc (I.lower i) (I.upper i) ∧ y i ≤ (I.lower i + I.upper i) / 2
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>n✝ : ℕ<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hx : x ∈ s<VAR>h✝ : UniqueDiffOn 𝕜 s<VAR>f✝ g : 𝕜 → F<VAR>n : ℕ<VAR>f : 𝕜 → 𝕜<VAR>h : ContDiff 𝕜 (↑n) f<VAR>c : 𝕜<GOAL>(iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n * iteratedDeriv n f (c * x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : Nontrivial R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalSemiring R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : TopologicalSpace A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>hf : autoParam (ContinuousOn f (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>S : Type u_3<VAR>inst✝⁴ : SMulZeroClass S R<VAR>inst✝³ : ContinuousConstSMul S R<VAR>inst✝² : SMulZeroClass S A<VAR>inst✝¹ : IsScalarTower S R A<VAR>inst✝ : IsScalarTower S R (R → R)<VAR>s : S<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfcₙ (fun x => s • x) a = s • a
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>homologyMap' e.hom h₁ h₂ ≫ homologyMap' e.inv h₂ h₁ = 𝟙 h₁.left.H
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<GOAL>homologyMap' e.inv h₂ h₁ ≫ homologyMap' e.hom h₁ h₂ = 𝟙 h₂.left.H
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>f : F[X]<VAR>q : ℕ<VAR>inst✝ : ExpChar F q<VAR>hm✝ : f.Monic<VAR>x✝ : ∃ m n y, m ≠ 0 ∧ f = (X ^ q ^ n - C y) ^ m<VAR>m n : ℕ<VAR>y : F<VAR>hm : m ≠ 0<VAR>h : f = (X ^ q ^ n - C y) ^ m<GOAL>f.natSepDegree = 1
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<GOAL>Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<VAR>ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)<GOAL>Function.Exact ⇑(lTensor M f) ⇑(lTensor M g)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>N✝ : Type w<VAR>inst✝⁸ : AddCommGroup N✝<VAR>inst✝⁷ : Module R N✝<VAR>inst✝⁶ : Small.{v, u} R<VAR>flat : Flat R M<VAR>N N' N'' : Type v<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup N''<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R N''<VAR>f : N →ₗ[R] N'<VAR>g : N' →ₗ[R] N''<VAR>exact : Function.Exact ⇑f ⇑g<VAR>π : N' →ₗ[R] N' ⧸ range f := (range f).mkQ<VAR>ι : N' ⧸ range f →ₗ[R] N'' := (range g).subtype ∘ₗ ↑g.quotKerEquivRange ∘ₗ ↑((range f).quotEquivOfEq (ker g) ⋯)<GOAL>Function.Exact ⇑(lTensor M f) ⇑(lTensor M π)
<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 b : X<VAR>γ : Path a b<GOAL>γ.extend (min 1 1) = b
<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 b : X<VAR>γ : Path a b<GOAL>γ.truncate 1 1 = (refl b).cast ⋯ ⋯
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>inst✝¹² : Monoid R<VAR>inst✝¹¹ : Monoid S<VAR>inst✝¹⁰ : Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : DistribMulAction R A<VAR>inst✝⁷ : NonUnitalNonAssocSemiring B<VAR>inst✝⁶ : DistribMulAction S B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : DistribMulAction T C<VAR>φ' : S →* R<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>B₁ : Type u_2<VAR>inst✝³ : NonUnitalNonAssocSemiring B₁<VAR>inst✝² : DistribMulAction R B₁<VAR>inst✝¹ : DistribMulAction R B<VAR>inst✝ : DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<GOAL>{ toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯ }.toFun 0 = 0
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>inst✝¹² : Monoid R<VAR>inst✝¹¹ : Monoid S<VAR>inst✝¹⁰ : Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : DistribMulAction R A<VAR>inst✝⁷ : NonUnitalNonAssocSemiring B<VAR>inst✝⁶ : DistribMulAction S B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : DistribMulAction T C<VAR>φ' : S →* R<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>B₁ : Type u_2<VAR>inst✝³ : NonUnitalNonAssocSemiring B₁<VAR>inst✝² : DistribMulAction R B₁<VAR>inst✝¹ : DistribMulAction R B<VAR>inst✝ : DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<VAR>x y : A<GOAL>{ toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯ }.toFun (x + y) = { toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯ }.toFun x + { toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯ }.toFun y
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>inst✝¹² : Monoid R<VAR>inst✝¹¹ : Monoid S<VAR>inst✝¹⁰ : Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : DistribMulAction R A<VAR>inst✝⁷ : NonUnitalNonAssocSemiring B<VAR>inst✝⁶ : DistribMulAction S B<VAR>inst✝⁵ : NonUnitalNonAssocSemiring C<VAR>inst✝⁴ : DistribMulAction T C<VAR>φ' : S →* R<VAR>ψ : S →* T<VAR>χ : R →* T<VAR>B₁ : Type u_2<VAR>inst✝³ : NonUnitalNonAssocSemiring B₁<VAR>inst✝² : DistribMulAction R B₁<VAR>inst✝¹ : DistribMulAction R B<VAR>inst✝ : DistribMulAction R C<VAR>f : A →ₙₐ[R] B<VAR>g : A →ₙₐ[R] C<VAR>x y : A<GOAL>{ toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun (x * y) = { toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun x * { toFun := Pi.prod ⇑f ⇑g, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }.toFun y