ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>a : Over S.X₁<VAR>ha' : ⟦a⟧ = a'<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<VAR>z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f<VAR>hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<VAR>z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f<VAR>hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q<VAR>j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<VAR>z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f<VAR>hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q<VAR>j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>pe : Epi j<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<VAR>z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f<VAR>hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q<VAR>j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>pe : Epi j<VAR>this : IsIso j<GOAL>kernel.ι S.g ≫ cokernel.π S.f = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<VAR>hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b<VAR>this✝ : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0<VAR>a' : Pseudoelement S.X₁<VAR>a : Over S.X₁<VAR>ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))<VAR>ha' : ⟦a⟧ = a'<VAR>Z : C<VAR>r : Z ⟶ ((fun g => app S.f g) a).left<VAR>q : Z ⟶ (Over.mk (kernel.ι S.g)).left<VAR>w✝ : Epi r<VAR>eq : Epi q<VAR>comm : r ≫ ((fun g => app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom<VAR>z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f<VAR>hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q<VAR>j : pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ⟶ kernel S.g := pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)<VAR>pe : Epi j<VAR>this : IsIso j<GOAL>((asIso j).inv ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) ≫ kernel.ι (cokernel.π S.f)) ≫ cokernel.π S.f = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>0 < ⌈a⌉ ↔ 0 < a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∃ b, derivFamily (o.familyOfBFamily f) b = a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>(∀ (i : Ordinal.{u}) (hi : i < o), f i hi a ≤ a) ↔ ∀ (i : (Quotient.out o).α), o.familyOfBFamily f i a ≤ a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max u v}<GOAL>∀ (i : (Quotient.out o).α), IsNormal (o.familyOfBFamily f i)
<GOAL>↑T⁻¹ = !![1, -1; 0, 1]
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : AddGroup N<VAR>f f₁ f₂ g g₁ g₂ : α →₀ N<GOAL>(f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>g : γ → δ<VAR>f' : α' → β → δ<VAR>g' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b<GOAL>g '' image2 f ↑s ↑t = image2 f' (g' '' ↑s) ↑t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : InvolutiveInv α<VAR>s✝ : Finset α<VAR>a : α<VAR>s : Finset α<GOAL>↑(s.preimage (fun x => x⁻¹) ⋯) = ↑s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeInf α<VAR>inst✝² : SemilatticeInf β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a : α<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : InfHomClass F α β<VAR>f : F<GOAL>InfClosed (range ⇑f)
<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>α : E<VAR>halg : IsAlgebraic F α<GOAL>finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
<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>α : E<VAR>halg : IsAlgebraic F α<VAR>this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }<GOAL>finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree
<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>α : E<VAR>halg : IsAlgebraic F α<VAR>this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }<GOAL>Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } = Fintype.card { x // x ∈ ((minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯)).toFinset }
<VAR>α : Type u_1<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s : Multiset α<VAR>a : α<GOAL>∀ (a_1 : α) (s : Multiset α), (s.sup ≤ a ↔ ∀ b ∈ s, b ≤ a) → ((a_1 ::ₘ s).sup ≤ a ↔ ∀ b ∈ a_1 ::ₘ s, b ≤ a)
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>x : Ei 0<VAR>m : (i : Fin n) → Ei i.succ<GOAL>‖f‖ * ∏ i : Fin (n + 1), ‖Fin.cons x m i‖ = ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>n : ℕ<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>Ei : Fin n.succ → Type wEi<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁴ : Fintype ι<VAR>inst✝¹³ : Fintype ι'<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁ i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁷ : (i : ι') → NormedAddCommGroup (E' i)<VAR>inst✝⁶ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁵ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)<VAR>inst✝⁴ : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : ContinuousMultilinearMap 𝕜 Ei G<VAR>x : Ei 0<VAR>m : (i : Fin n) → Ei i.succ<GOAL>‖f‖ * (‖Fin.cons x m 0‖ * ∏ i : Fin n, ‖Fin.cons x m i.succ‖) = ‖f‖ * ‖x‖ * ∏ i : Fin n, ‖m i‖
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>(norm R) ((algebraMap R S) x) = x ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>((toMatrix b b) ((lsmul R R S) x)).det = x ^ Fintype.card ι
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>(toMatrix b b) ((lsmul R R S) x) = diagonal fun x_1 => x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : Algebra K F<VAR>ι : Type w<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>x : R<VAR>this : DecidableEq ι<GOAL>x ^ Fintype.card ι = ∏ i : ι, x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<VAR>n : ℕ<GOAL>Chebyshev.T R ↑n = C ⅟2 * (dickson 1 1 n).comp (2 * X)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>inst✝ : Invertible 2<VAR>n : ℕ<GOAL>Chebyshev.T R ↑n = C ⅟2 * (↑2 * (Chebyshev.T R ↑n).comp (C ⅟2 * (2 * X)))
<VAR>R : Type u<VAR>S : Type v<VAR>a✝ b c d : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a : R<VAR>m : ℕ<GOAL>((monomial m) a).natDegree ≤ m
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<GOAL>a ^ 2 < 1 ↔ |a| < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : Continuous f<VAR>a : α<GOAL>IntegrableAtFilter f (𝓝 a) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : SecondCountableTopologyEither α E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : α → E<VAR>hf : Continuous f<VAR>a : α<GOAL>IntegrableAtFilter f (𝓝[univ] a) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hf : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg : IntegrableAtFilter g l μ<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hf : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg : IntegrableAtFilter g l μ<VAR>C : ℝ<VAR>hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hf✝ : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg✝ : IntegrableAtFilter g l μ<VAR>C : ℝ<VAR>hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖<VAR>hf : AEStronglyMeasurable f (μ.restrict s)<VAR>hg : IntegrableOn g s μ<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hf✝ : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg✝ : IntegrableAtFilter g l μ<VAR>C : ℝ<VAR>hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖<VAR>hf : AEStronglyMeasurable f (μ.restrict s)<VAR>hg : IntegrableOn g s μ<GOAL>∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hf✝ : f =O[l] g<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hg✝ : IntegrableAtFilter g l μ<VAR>C : ℝ<VAR>hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖<VAR>hf : AEStronglyMeasurable f (μ.restrict s)<VAR>hg : IntegrableOn g s μ<VAR>x : α<VAR>hx : x ∈ s<GOAL>‖f x‖ ≤ ‖C * ‖g x‖‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 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>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a • x‖₊ ∂μ = (∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 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>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ * ↑‖x‖₊ ∂μ = (∫⁻ (a : α) in t, ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊ ∂μ) * ↑‖x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : 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 E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 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>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>Measurable fun a => ↑‖↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)) a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>x✝ : Fin (n + 1)<GOAL>x✝ ∈ ↑(Iio (last n)) ↔ x✝ ∈ ↑(map castSuccEmb univ)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>π : ι → Set (Set Ω)<VAR>m : ι → MeasurableSpace Ω<VAR>x✝ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>S : Finset ι<VAR>s : ι → Set Ω<VAR>inst✝ : Fintype ι<VAR>h : iIndepSets π μ<VAR>hs : ∀ (i : ι), s i ∈ π i<GOAL>μ (⋂ i, s i) = ∏ i : ι, μ (s i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∀ᵐ (x : α) ∂μ, f x < ⊤<GOAL>0 ≤ᶠ[ae μ] fun x => (f x).toReal
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (α i)<VAR>this : Encodable ι<GOAL>(Measure.pi μ) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s : Set α<VAR>f g : α → ℝ≥0∞<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ