ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom = (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<GOAL>(coeff R d) (f ^ n) = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<GOAL>∑ l ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff R (l i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<GOAL>∀ x ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff R (x i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : k ∈ (range n).finsuppAntidiag d<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>∏ i ∈ range n, (coeff R (k i)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(∏ x ∈ range n \ s, (coeff R (k x)) f) * ∏ x ∈ s, (coeff R (k x)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>∏ x ∈ s, (coeff R (k x)) f = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(constantCoeff σ R) f ^ s.card = 0
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>m ≤ s.card
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>m + (range n \ Finset.filter (fun i => k i = 0) (range n)).card ≤ n
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>m + (range n \ Finset.filter (fun i => k i = 0) (range n)).card ≤ m + d.degree
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(range n \ Finset.filter (fun i => k i = 0) (range n)).card ≤ (∑ x ∈ range n \ s, k x).degree
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(range n \ s).card ≤ (∑ x ∈ range n \ s, k x).degree
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(range n \ s).card = (range n \ s).card • 1
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>(∑ x ∈ range n \ s, k x).degree = ∑ x ∈ range n \ s, (k x).degree
<VAR>σ : Type u_1<VAR>R✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>ι : Type u_4<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : DecidableEq σ<VAR>f : MvPowerSeries σ R<VAR>m : ℕ<VAR>hf : (constantCoeff σ R) f ^ m = 0<VAR>d : σ →₀ ℕ<VAR>n : ℕ<VAR>hn : m + d.degree ≤ n<VAR>k : ℕ →₀ σ →₀ ℕ<VAR>hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n<VAR>s : Finset ℕ := Finset.filter (fun i => k i = 0) (range n)<VAR>hs_def : s = Finset.filter (fun i => k i = 0) (range n)<VAR>hs : s ⊆ range n<VAR>hs' : ∀ i ∈ s, (coeff R (k i)) f = (constantCoeff σ R) f<VAR>hs'' : ∀ i ∈ s, k i = 0<GOAL>∀ x ∈ range n \ s, 1 ≤ (fun x => (k x).degree) x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : f x ≠ 0<VAR>hg : g x ≠ 0<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>hdg : DifferentiableAt 𝕜 g x<GOAL>logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>f g : 𝕜 → 𝕜'<VAR>x : 𝕜<VAR>hf : f x ≠ 0<VAR>hg : g x ≠ 0<VAR>hdf : DifferentiableAt 𝕜 f x<VAR>hdg : DifferentiableAt 𝕜 g x<GOAL>(deriv f x * g x + f x * deriv g x) / (f x * g x) = deriv f x / f x + deriv g x / g x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>s : Set X<VAR>a : X<GOAL>a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : FrechetUrysohnSpace X<VAR>s : Set X<VAR>a : X<GOAL>a ∈ seqClosure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Tendsto x atTop (𝓝 a)
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z
<GOAL>cos (↑π / 2) = ↑(Real.cos (π / 2))
<GOAL>cos (↑π / 2) = cos ↑(π / 2)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<GOAL>‖m.prod‖ ≤ (Multiset.map (fun x => ‖x‖) m).sum
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<GOAL>Multiplicative.ofAdd ‖m.prod‖ ≤ (Multiset.map (⇑Multiplicative.ofAdd ∘ fun x => ‖x‖) m).prod
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<GOAL>(⇑Multiplicative.ofAdd ∘ norm) 1 = 1
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>m : Multiset E<VAR>x y : E<GOAL>(⇑Multiplicative.ofAdd ∘ norm) (x * y) ≤ (⇑Multiplicative.ofAdd ∘ norm) x * (⇑Multiplicative.ofAdd ∘ norm) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<GOAL>UniformContinuous ⇑toFun
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<GOAL>∀ (i : α), UniformContinuous fun x => toFun x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>x : α<GOAL>UniformContinuous fun x_1 => toFun x_1 x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝³ : EquivLike F α β<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>e : M ≃* N<VAR>f : P →* M<GOAL>(↑e.symm).comp ((↑e).comp f) = f
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(z - x) * f y ≤ (z - y) * f x + (y - x) * f z
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 ≤ (z - y) / (z - x)<VAR>hb : 0 ≤ (y - x) / (z - x)<GOAL>f y ≤ ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 ≤ (z - y) / (z - x)<VAR>hb : 0 ≤ (y - x) / (z - x)<GOAL>f y = f ((z - y) / (z - x) * x + (y - x) / (z - x) * z)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 ≤ (z - y) / (z - x)<VAR>hb : 0 ≤ (y - x) / (z - x)<GOAL>(z - y) / (z - x) + (y - x) / (z - x) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : ConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxy' : 0 < y - x<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<VAR>ha : 0 ≤ (z - y) / (z - x)<VAR>hb : 0 ≤ (y - x) / (z - x)<GOAL>(z - y) / (z - x) * f x + (y - x) / (z - x) * f z = ((z - y) * f x + (y - x) * f z) / (z - x)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurveAt γ v t₀<VAR>dt : ℝ<GOAL>IsIntegralCurveAt (γ ∘ fun x => x + dt) v (t₀ - dt)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)<VAR>dt : ℝ<GOAL>∃ ε > 0, IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<GOAL>IsIntegralCurveOn (γ ∘ fun x => x + dt) v (Metric.ball (t₀ - dt) ε)
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<GOAL>Metric.ball (t₀ - dt) ε = {t | t + dt ∈ Metric.ball t₀ ε}
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ dt ε : ℝ<VAR>hε : ε > 0<VAR>h : IsIntegralCurveOn γ v (Metric.ball t₀ ε)<VAR>t : ℝ<GOAL>t ∈ Metric.ball (t₀ - dt) ε ↔ t ∈ {t | t + dt ∈ Metric.ball t₀ ε}
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(C a * p).degree = p.degree
<VAR>x x' : PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x ≤ x'<GOAL>(x.insertRight x').Numeric
<VAR>x x' : PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x ≤ x'<GOAL>(-(-x).insertLeft (-x')).Numeric
<VAR>x x' : PGame<VAR>x_num : x.Numeric<VAR>x'_num : x'.Numeric<VAR>h : x ≤ x'<GOAL>((-x).insertLeft (-x')).Numeric
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℕ<VAR>n : ℕ<GOAL>(∃ s ∈ l.ranges, n ∈ s) ↔ n < l.sum
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>U : Submodule 𝕜 E<VAR>V : Set (Submodule 𝕜 E)<GOAL>(∀ Uᵢ ∈ V, Uᵢ ⟂ U) ↔ ∀ Vᵢ ∈ V, U ⟂ Vᵢ
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<GOAL>toUnitHom ((changeLevel ⋯) χ) = toUnitHom χ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<GOAL>WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m<VAR>x : α<GOAL>Acc r x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m<VAR>x : α<VAR>hx : ¬Acc r x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m<VAR>x : α<VAR>hx : ¬Acc r x<VAR>m : α<VAR>hm : m ∈ {x | ¬Acc r x}<VAR>hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m<VAR>y : α<VAR>hy : r y m<GOAL>Acc r y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ r' r : α → α → Prop<VAR>h : ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m<VAR>x : α<VAR>hx : ¬Acc r x<VAR>m : α<VAR>hm : m ∈ {x | ¬Acc r x}<VAR>hm' : ∀ x ∈ {x | ¬Acc r x}, ¬r x m<VAR>y : α<VAR>hy : r y m<VAR>hy' : ¬Acc r y<GOAL>False
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>evenOddRec h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n)
<VAR>P : ℕ → Sort u_1<VAR>h0 : P 0<VAR>h_even : (i : ℕ) → P i → P (2 * i)<VAR>h_odd : (i : ℕ) → P i → P (2 * i + 1)<VAR>H : h_even 0 h0 = h0<VAR>n : ℕ<GOAL>(match false, 0, h0 with | false, i, hi => h_even i hi | true, i, hi => h_odd i hi) = h0 ∨ (n = 0 → false = true)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.Φ n).coeff (n.natAbs ^ 2) = 1
<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 c : X<VAR>γ₁ : Path a b<VAR>γ₂ : Path b c<GOAL>range ⇑{ toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } = range ⇑γ₁ ∪ range ⇑γ₂
<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 c : X<VAR>γ₁ : Path a b<VAR>γ₂ : Path b c<GOAL>range ⇑{ toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } ⊆ range ⇑γ₁ ∪ range ⇑γ₂
<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 c : X<VAR>γ₁ : Path a b<VAR>γ₂ : Path b c<GOAL>range ⇑γ₁ ∪ range ⇑γ₂ ⊆ range ⇑{ toFun := (fun t => if t ≤ 1 / 2 then γ₁.extend (2 * t) else γ₂.extend (2 * t - 1)) ∘ Subtype.val, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y Z : C<VAR>f : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : Ring α<VAR>a✝ b✝ a b : α<VAR>u : αˣ<GOAL>a /ₚ u + b = (a + b * ↑u) /ₚ u