ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>y : β<GOAL>(sum fun i => (sFiniteSeq μ i).prod (dirac y)) = sum fun i => map (fun x => (x, y)) (sFiniteSeq μ i)
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>y : β<VAR>i : ℕ<GOAL>(sFiniteSeq μ i).prod (dirac y) = map (fun x => (x, y)) (sFiniteSeq μ i)
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>y : β<VAR>i : ℕ<VAR>s : Set α<VAR>t : Set β<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<GOAL>(map (fun x => (x, y)) (sFiniteSeq μ i)) (s ×ˢ t) = (sFiniteSeq μ i) s * (dirac y) t
<VAR>α : Type u_1<VAR>s✝¹ t✝ : Finset α<VAR>n : ?m.18500<VAR>s✝ t s : Finset α<GOAL>Multiset.map val (powersetCard 1 s).val = Multiset.map val (map { toFun := singleton, inj' := ⋯ } s).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a : α<GOAL>IsUpperSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Ici a ⊆ s
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>k : ℕ<GOAL>multichoose 2 k = ↑k + 1
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<GOAL>(f x - f a) / (x - a) < (f y - f a) / (y - a)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa✝ : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<VAR>hxa : x < a<GOAL>(f x - f a) / (x - a) < (f y - f a) / (y - a)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>a x y : 𝕜<VAR>ha : a ∈ s<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxa✝ : x ≠ a<VAR>hya : y ≠ a<VAR>hxy : x < y<VAR>hxa : x > a<GOAL>(f x - f a) / (x - a) < (f y - f a) / (y - a)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<GOAL>atTop = generate (Ici '' s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<VAR>x : α<GOAL>∃ y ∈ s, x ≤ y
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrder α<VAR>s : Set α<VAR>hs : ¬BddAbove s<VAR>x y : α<VAR>hy : y ∈ s<VAR>hy' : x < y<GOAL>∃ y ∈ s, x ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a b : α<VAR>h : a < b<VAR>s : Set α<GOAL>[s ∈ 𝓝[≤] b, s ∈ 𝓝[Icc a b] b, s ∈ 𝓝[Ioc a b] b, ∃ l ∈ Ico a b, Ioc l b ⊆ s, ∃ l ∈ Iio b, Ioc l b ⊆ s].TFAE
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀<GOAL>whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>e : toKaroubi (ChainComplex C ℕ) ⋙ Γ₂ ⋙ N₂ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 (Karoubi (ChainComplex C ℕ)) := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀<VAR>h : ((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).map (((whiskeringLeft (ChainComplex C ℕ) (Karoubi (ChainComplex C ℕ)) (Karoubi (ChainComplex C ℕ))).obj (toKaroubi (ChainComplex C ℕ))).preimage e.hom) = e.hom<GOAL>whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom
<VAR>z✝ y x✝ : ℝ<VAR>x z : ℂ<VAR>hz : ‖z‖ ≤ 1<GOAL>cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
<VAR>z✝ y x✝ : ℝ<VAR>x z : ℂ<VAR>hz : ‖z‖ ≤ 1<GOAL>cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>h : 0 < x<VAR>h₁ : 0 < y<GOAL>logb b x ≤ logb b y ↔ x ≤ y
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>a : α<VAR>σ : Perm β<VAR>x✝¹ : α × β<VAR>a' : α<VAR>b : β<VAR>hab : (prodExtendRight a σ) (a', b) ≠ (a', b)<VAR>x✝ : (prodExtendRight a σ) ((prodExtendRight a σ) (a', b)) ≠ (prodExtendRight a σ) (a', b)<GOAL>(fun ab x => ab.2) ((prodExtendRight a σ) (a', b)) x✝ = σ ((fun ab x => ab.2) (a', b) hab)
<VAR>α : Type u<VAR>inst✝³ : DecidableEq α<VAR>β : Type v<VAR>inst✝² : Fintype α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : Fintype β<VAR>a : α<VAR>σ : Perm β<VAR>x✝¹ x✝ : α × β<VAR>a₁ : α<VAR>b₁ : β<VAR>hab₁ : (prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)<VAR>a₂ : α<VAR>b₂ : β<VAR>hab₂ : (prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)<VAR>h : (fun ab x => ab.2) (a₁, b₁) hab₁ = (fun ab x => ab.2) (a₂, b₂) hab₂<GOAL>(a₁, b₁) = (a₂, b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CharZero α<VAR>m n : ℕ<GOAL>↑n < 1 ↔ n = 0
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<GOAL>∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>x : ℚ_[p]<VAR>hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε<GOAL>∃ q, ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑f i - q) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>x : ℚ_[p]<VAR>hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<GOAL>padicNormE (↑f i - x) < ε
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>f : CauSeq ℚ_[p] ⇑padicNormE<VAR>x : ℚ_[p]<VAR>hx : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (x - ↑f i) < ε<VAR>ε : ℚ<VAR>hε : ε > 0<VAR>N : ℕ<VAR>hN : ∀ i ≥ N, padicNormE (x - ↑f i) < ε<VAR>i : ℕ<VAR>hi : i ≥ N<GOAL>padicNormE (x - ↑f i) < ε
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>IsLprojection X (P + Q - P * Q)
<VAR>X : Type u_1<VAR>inst✝³ : NormedAddCommGroup X<VAR>M : Type u_2<VAR>inst✝² : Ring M<VAR>inst✝¹ : Module M X<VAR>inst✝ : FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>P + Q - P * Q = 1 - (1 - P) * (1 - Q)
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : (p * p.mirror).leadingCoeff = (q * q.mirror).leadingCoeff<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : eval 1 (p * p.mirror) = eval 1 (q * q.mirror)<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : eval 1 (trinomial k m n ↑u ↑v ↑w) ^ 2 = eval 1 (trinomial k m' n ↑x ↑v ↑z) ^ 2<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : (↑u + ↑v + ↑w) ^ 2 = (↑x + ↑v + ↑z) ^ 2<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : (↑v + (↑w + ↑u)) ^ 2 = (↑v + (↑z + ↑x)) ^ 2<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : 2 * ↑w * ↑u + 2 * ↑v * (↑w + ↑u) = 2 * ↑z * ↑x + 2 * ↑v * (↑z + ↑x)<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : ↑w + ↑u = ↑z + ↑x<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : ↑w = ↑z ∧ ↑u = ↑x ∨ ↑w = ↑x ∧ ↑u = ↑z<GOAL>q = p ∨ q = p.mirror
<VAR>p q : ℤ[X]<VAR>k m m' n : ℕ<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hkm' : k < m'<VAR>hmn' : m' < n<VAR>u v w x z : ℤˣ<VAR>hp : p = trinomial k m n ↑u ↑v ↑w<VAR>hq : q = trinomial k m' n ↑x ↑v ↑z<VAR>h : p * p.mirror = q * q.mirror<VAR>hmul : ↑w * ↑u = ↑z * ↑x<VAR>hadd : w = z ∧ u = x ∨ w = x ∧ u = z<GOAL>q = p ∨ q = p.mirror
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.697927) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>0 ≤ cfc f a ↔ ∀ x ∈ spectrum R a, 0 ≤ f x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type u_1) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>f : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>(∀ (a_1 : ↑(spectrum R a)), 0 a_1 ≤ { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ } a_1) ↔ ∀ x ∈ spectrum R a, 0 ≤ f x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>hz : ‖z‖ = 1<GOAL>(starRingEnd K) z * z = 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r✝ p : R[X]<VAR>n d : ℕ<VAR>r : R<GOAL>(p * (monomial n) r).coeff (d + n) = p.coeff d * r
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ : C<VAR>inst✝ : HasPushouts C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>x x' : Under X<VAR>u : x ⟶ x'<GOAL>x.hom ≫ u.right ≫ pushout.inl x'.hom f = f ≫ pushout.inr x'.hom f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ F₂ : BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<GOAL>B₂.IsPairSelfAdjoint F₂ f ↔ (B₂.comp ↑e ↑e).IsPairSelfAdjoint (F₂.comp ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ F₂ : BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e<GOAL>B₂.IsPairSelfAdjoint F₂ f ↔ (B₂.comp ↑e ↑e).IsPairSelfAdjoint (F₂.comp ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ F₂ : BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e<VAR>hᵣ : (B₂.comp ↑e ↑e).compRight (e.symm.conj f) = (B₂.compRight f).comp ↑e ↑e<GOAL>B₂.IsPairSelfAdjoint F₂ f ↔ (B₂.comp ↑e ↑e).IsPairSelfAdjoint (F₂.comp ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ F₂ : BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e<VAR>hᵣ : (B₂.comp ↑e ↑e).compRight (e.symm.conj f) = (B₂.compRight f).comp ↑e ↑e<VAR>he : Function.Surjective ⇑↑e<GOAL>B₂.IsPairSelfAdjoint F₂ f ↔ (B₂.comp ↑e ↑e).IsPairSelfAdjoint (F₂.comp ↑e ↑e) (e.symm.conj f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝¹² : Field K<VAR>inst✝¹¹ : AddCommGroup V<VAR>inst✝¹⁰ : Module K V<VAR>M'✝ : Type u_7<VAR>M''✝ : Type u_8<VAR>inst✝⁹ : AddCommMonoid M'✝<VAR>inst✝⁸ : AddCommMonoid M''✝<VAR>inst✝⁷ : Module R M'✝<VAR>inst✝⁶ : Module R M''✝<VAR>B : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>F : BilinForm R M<VAR>M' : Type u_9<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>B' : BilinForm R M'<VAR>f✝ f' : M →ₗ[R] M'<VAR>g g' : M' →ₗ[R] M<VAR>M₁' : Type u_10<VAR>inst✝³ : AddCommGroup M₁'<VAR>inst✝² : Module R₁ M₁'<VAR>B₁' : BilinForm R₁ M₁'<VAR>f₁ f₁' : M₁ →ₗ[R₁] M₁'<VAR>g₁ g₁' : M₁' →ₗ[R₁] M₁<VAR>B₂' : BilinForm R M'<VAR>f₂ f₂' : M →ₗ[R] M'<VAR>g₂ g₂' : M' →ₗ[R] M<VAR>M'' : Type u_11<VAR>inst✝¹ : AddCommMonoid M''<VAR>inst✝ : Module R M''<VAR>B'' : BilinForm R M''<VAR>B₂ F₂ : BilinForm R M<VAR>e : M' ≃ₗ[R] M<VAR>f : Module.End R M<VAR>hₗ : (F₂.comp ↑e ↑e).compLeft (e.symm.conj f) = (F₂.compLeft f).comp ↑e ↑e<VAR>hᵣ : (B₂.comp ↑e ↑e).compRight (e.symm.conj f) = (B₂.compRight f).comp ↑e ↑e<VAR>he : Function.Surjective ⇑↑e<GOAL>B₂.IsAdjointPair F₂ f f ↔ (B₂.comp ↑e ↑e).IsAdjointPair (F₂.comp ↑e ↑e) (e.symm.conj f) (e.symm.conj f)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x✝ y✝ : E<VAR>x y : Set E<GOAL>↑1 * EMetric.diam x + ↑1 * EMetric.diam y = EMetric.diam x + EMetric.diam y
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : P →ₗ[R] M<GOAL>(trace R P) (g ∘ₗ f ∘ₗ h) = (trace R N) (f ∘ₗ h ∘ₗ g)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>y : M<VAR>hy : y ∈ S<GOAL>(f.domRestrict S) ⟨y, hy⟩ ∈ range f
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>x y : R<VAR>r : ℝ<VAR>inst✝ : Ring R<VAR>p : RingSeminorm R<VAR>hp : p 1 ≤ 1<GOAL>p 1 = 1 ↔ p ≠ 0
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>x y : R<VAR>r : ℝ<VAR>inst✝ : Ring R<VAR>p : RingSeminorm R<VAR>hp : p 1 ≤ 1<VAR>h : p ≠ 0<GOAL>p 1 = 1
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>x y : R<VAR>r : ℝ<VAR>inst✝ : Ring R<VAR>p : RingSeminorm R<VAR>hp : p 1 ≤ 1<VAR>h : p ≠ 0<VAR>hp0 : p 1 = 0<GOAL>p 1 = 1
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>x y : R<VAR>r : ℝ<VAR>inst✝ : Ring R<VAR>p : RingSeminorm R<VAR>hp : p 1 ≤ 1<VAR>h : p ≠ 0<VAR>hp0 : 0 < p 1<GOAL>p 1 = 1
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>c : α → β<VAR>h : ∀ (a b : α), c a = c b<VAR>this : (fun x => (c x.1, c x.2)) ⁻¹' idRel = univ<GOAL>𝓤 α ≤ comap (fun x => (c x.1, c x.2)) (𝓟 idRel)
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝¹ : SemilatticeSup L<VAR>inst✝ : ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x<GOAL>ContinuousWithinAt (s.sup' hne f) t x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (h x) L'<VAR>hh : HasDerivAtFilter h h' x L<VAR>hL : Tendsto h L L'<VAR>hy : y = h x<GOAL>HasDerivAtFilter (h₂ ∘ h) (h₂' * h') x L
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>m₁ m₂ m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → E<VAR>hle₁ : m₁ ≤ m<VAR>hle₂ : m₂ ≤ m<VAR>inst✝ : SigmaFinite (μ.trim hle₂)<VAR>hf : StronglyMeasurable f<VAR>hindp : Indep m₁ m₂ μ<VAR>hfint : Integrable f μ<GOAL>μ[f|m₂] =ᶠ[ae μ] fun x => ∫ (x : Ω), f x ∂μ