ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : Ring A<VAR>inst✝¹⁰ : PartialOrder A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : StarOrderedRing A<VAR>inst✝⁷ : Algebra ℝ A<VAR>inst✝⁶ : TopologicalRing A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : StarModule ℝ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun x => 0 ≤ x<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>ha : 0 ≤ a<GOAL>cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
<VAR>A : Type u_1<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : Ring A<VAR>inst✝¹⁰ : PartialOrder A<VAR>inst✝⁹ : StarRing A<VAR>inst✝⁸ : StarOrderedRing A<VAR>inst✝⁷ : Algebra ℝ A<VAR>inst✝⁶ : TopologicalRing A<VAR>inst✝⁵ : ContinuousStar A<VAR>inst✝⁴ : StarModule ℝ A<VAR>inst✝³ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝² : ContinuousFunctionalCalculus ℝ≥0 fun x => 0 ≤ x<VAR>inst✝¹ : UniqueContinuousFunctionalCalculus ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>ha : 0 ≤ a<VAR>this : CompactSpace ↑(σ ℝ a)<GOAL>cfcHom ha = SpectrumRestricts.starAlgHom (cfcHom ⋯) ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>x : α<GOAL>(∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis p s<VAR>x : α<GOAL>(∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.26109, u_3} E<VAR>inst✝⁴ : Category.{?u.26113, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.26109, u_3} E<VAR>inst✝⁴ : Category.{?u.26113, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>a : A<VAR>X : C<GOAL>(isoWhiskerLeft (F.functor a) (shiftFunctorZero D A)).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>G : Cᵒᵖ ⥤ Grp<VAR>X : C<VAR>I : Type w'<VAR>U : I → C<VAR>γ₁ γ₂ γ₃ : OneCochain G U<VAR>α β : ZeroCochain G U<VAR>h₁₂ : OneCohomologyRelation γ₁ γ₂ α<VAR>h₂₃ : OneCohomologyRelation γ₂ γ₃ β<VAR>i j : I<VAR>T : C<VAR>a : T ⟶ U i<VAR>b : T ⟶ U j<GOAL>(G.map a.op) (β i * α i) * γ₁.ev i j a b = γ₃.ev i j a b * (G.map b.op) (β j * α j)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ε =o[atTop] fun x => 1<GOAL>∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖<GOAL>∀ᶠ (n : ℕ) in atTop, 0 < 1 + ε ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖<GOAL>∀ᶠ (x : ℝ) in atTop, (fun n => 0 < 1 + ε n) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖<VAR>x : ℝ<VAR>a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖<VAR>hx' : 1 < x<GOAL>0 < 1 + ε x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : ℝ) in atTop, ‖ε x‖ ≤ c * ‖1‖<VAR>x : ℝ<VAR>a✝ : ‖ε x‖ ≤ 1 / 2 * ‖1‖<VAR>hx' : 1 < x<VAR>this : 0 < log x<GOAL>0 < 1 + ε x
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{max u v}<VAR>i : ι<GOAL>f i ≤ sum f
<VAR>α β : Type u<VAR>β' : Type v<GOAL>#(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Linear R C<VAR>S₁ S₂ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>a : R<VAR>γ : LeftHomologyMapData φ h₁ h₂<GOAL>cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂
<VAR>a✝¹ a✝ : ℕ<GOAL>↑a✝¹ + ↑a✝ = 1 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>f : E → F<VAR>x : E<VAR>f' : E →L[ℝ] F<VAR>h : HasFDerivAt f f' x<GOAL>ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪f' u, f' v⟫_ℝ = c * ⟪u, v⟫_ℝ
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>f.lim ≠ 0
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<VAR>h₃ : f * f.inv hf * g = f * f.inv hf * g<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<VAR>h₃ : f * f.inv hf * g = f * f.inv hf * g<VAR>h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<VAR>h₃ : f * f.inv hf * g = f * f.inv hf * g<VAR>h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g<VAR>h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<VAR>h₃ : f * f.inv hf * g = f * f.inv hf * g<VAR>h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g<VAR>h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)<VAR>h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)<GOAL>(g - f * f.inv hf * g).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f✝ : CauSeq β abv<VAR>hf✝ : ¬f✝.LimZero<VAR>hl : f✝.lim ≠ 0<VAR>g f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>h₂ : g - f * f.inv hf * g = 1 * g - f * f.inv hf * g<VAR>h₃ : f * f.inv hf * g = f * f.inv hf * g<VAR>h₄ : g - f * f.inv hf * g = (1 - f * f.inv hf) * g<VAR>h₅ : g - f * f.inv hf * g = g * (1 - f * f.inv hf)<VAR>h₆ : g - f * f.inv hf * g = g * (1 - f.inv hf * f)<GOAL>(g * (1 - f.inv hf * f)).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>hl : f.lim ≠ 0<VAR>h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero<GOAL>(f.inv hf - const abv f.lim⁻¹ - (const abv f.lim - f) * (f.inv hf * const abv f.lim⁻¹)).LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Field β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>hf : ¬f.LimZero<VAR>hl : f.lim ≠ 0<VAR>h₁ : ∀ (g f : CauSeq β abv) (hf : ¬f.LimZero), (g - f * f.inv hf * g).LimZero<GOAL>(f.inv hf - const abv f.lim * (f.inv hf * const abv f.lim⁻¹) - (const abv f.lim⁻¹ - f * (f.inv hf * const abv f.lim⁻¹))).LimZero
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<GOAL>comap f ⊤ = ⊤
<VAR>k : Type u_1<VAR>V₁ : Type u_2<VAR>P₁ : Type u_3<VAR>V₂ : Type u_4<VAR>P₂ : Type u_5<VAR>V₃ : Type u_6<VAR>P₃ : Type u_7<VAR>inst✝⁹ : Ring k<VAR>inst✝⁸ : AddCommGroup V₁<VAR>inst✝⁷ : Module k V₁<VAR>inst✝⁶ : AffineSpace V₁ P₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module k V₂<VAR>inst✝³ : AffineSpace V₂ P₂<VAR>inst✝² : AddCommGroup V₃<VAR>inst✝¹ : Module k V₃<VAR>inst✝ : AffineSpace V₃ P₃<VAR>f : P₁ →ᵃ[k] P₂<GOAL>↑(comap f ⊤) = ↑⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<VAR>e : β ≃o γ<VAR>y : γ<GOAL>IsLUB {x | (⇑e ∘ f) x ≤ y} ((g ∘ ⇑e.symm) y)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>f : Arrow C<VAR>inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom<VAR>S : SplitEpi f.hom<VAR>n : ℕ<GOAL>(s f S n ≫ WidePullback.base fun x => f.hom) = WidePullback.base fun x => f.hom
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<GOAL>z.GammaSeq n * (1 - z).GammaSeq n = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<GOAL>↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 / ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<VAR>this : ↑n ^ z * ↑n ^ (1 - z) = ↑n<GOAL>↑n ^ z * ↑n ^ (1 - z) * ↑n ! ^ 2 / ((∏ j ∈ Finset.range (n + 1), (z + ↑j)) * ∏ j ∈ Finset.range (n + 1), (1 - z + ↑j)) = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<VAR>this : ↑n ^ z * ↑n ^ (1 - z) = ↑n<GOAL>↑n * ↑n ! ^ 2 / ((∏ x ∈ Finset.range n, (z + ↑(x + 1)) * (1 - z + ↑x)) * (z * (↑n + 1 - z))) = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<VAR>this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n<VAR>this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)<GOAL>↑n * ↑n ! ^ 2 / ((∏ x ∈ Finset.range n, (z + ↑(x + 1)) * (1 - z + ↑x)) * (z * (↑n + 1 - z))) = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<VAR>this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n<VAR>this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)<GOAL>↑n * ↑n ! ^ 2 / ((∏ x ∈ Finset.range n, ↑((x + 1) ^ 2) * (1 - z ^ 2 / (↑x + 1) ^ 2)) * (z * (↑n + 1 - z))) = ↑n / (↑n + 1 - z) * (1 / (z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)))
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>aux : ∀ (a b c d : ℂ), a * b * (c * d) = a * c * (b * d)<VAR>this✝ : ↑n ^ z * ↑n ^ (1 - z) = ↑n<VAR>this : ∀ (j : ℕ), (z + ↑(j + 1)) * (1 - z + ↑j) = ↑((j + 1) ^ 2) * (1 - z ^ 2 / (↑j + 1) ^ 2)<GOAL>↑n ! ^ 2 ≠ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>(η_ Y Y' ≫ f ▷ Y') ▷ Y ≫ (α_ Z Y' Y).hom ≫ Z ◁ ε_ Y Y' ≫ (ρ_ Z).hom = η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>η_ Y Y' ▷ Y ⊗≫ (f ▷ (Y' ⊗ Y) ≫ Z ◁ ε_ Y Y') ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>η_ Y Y' ▷ Y ⊗≫ (Y ◁ ε_ Y Y' ≫ f ▷ 𝟙_ C) ⊗≫ 𝟙 Z = (η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>(η_ Y Y' ▷ Y ⊗≫ Y ◁ ε_ Y Y') ⊗≫ f = (λ_ Y).hom ≫ f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y ⟶ Z<GOAL>⊗𝟙 ⊗≫ f = (λ_ Y).hom ≫ f
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a : α<VAR>q : ℚ≥0<VAR>ha : 0 ≤ a<GOAL>0 ≤ q • a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedSemifield α<VAR>a : α<VAR>q : ℚ≥0<VAR>ha : 0 ≤ a<GOAL>0 ≤ ↑q * a
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>α : Sort u_2<GOAL>⨅ x, 0 = 0
<VAR>ι : Sort u_1<VAR>f : ι → ℝ≥0<VAR>α : Sort u_2<GOAL>⨅ i, ↑0 = ↑0
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : Group G'<VAR>inst✝³ : Group G''<VAR>A : Type u_4<VAR>inst✝² : AddGroup A<VAR>H K✝ : Subgroup G<VAR>k : Set G<VAR>N : Type u_5<VAR>inst✝¹ : Group N<VAR>P : Type u_6<VAR>inst✝ : Group P<VAR>K : Subgroup N<VAR>x✝ : N<GOAL>x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K
<VAR>α : Type u_1<VAR>c₀ : RBColor<VAR>n₀ : Nat<VAR>c : RBColor<VAR>n : Nat<VAR>t : RBNode α<VAR>path : Path α<VAR>hp : Path.Balanced c₀ n₀ path c n<VAR>ht : RedRed (c = red) t n<GOAL>∃ n, (path.ins t).Balanced black n
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<GOAL>(Finset.Ioo s t).card = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s) - 2
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>M✝ : Type u_3<VAR>R : Type u_4<VAR>A : Type u_5<VAR>inst✝² : Monoid M✝<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>M N : AddSubmonoid R<GOAL>M * N = closure (↑M * ↑N)
<GOAL>∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.Finite
<VAR>R✝ S✝ : Type u_1<VAR>inst✝¹ : CommRing R✝<VAR>inst✝ : CommRing S✝<VAR>e✝ : R✝ ≃+* S✝<GOAL>e✝.toRingHom.Finite
<VAR>l : Filter ℂ<VAR>b₁ b₂ : ℝ<VAR>hl : IsExpCmpFilter l<VAR>hb : b₁ < b₂<VAR>m n : ℤ<GOAL>(fun z => z ^ m * cexp (↑b₁ * z)) =o[l] fun z => z ^ n * cexp (↑b₂ * z)
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable g (μ.withDensity fun x => ↑(AEMeasurable.mk f hf x))
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>(fun x => ↑(f x)) =ᶠ[ae μ] fun x => ↑(AEMeasurable.mk f hf x)
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<VAR>x : α<VAR>hx : f x = AEMeasurable.mk f hf x<GOAL>↑(f x) = ↑(AEMeasurable.mk f hf x)
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>Integrable (fun x => ↑(AEMeasurable.mk f hf x) • g x) μ ↔ Integrable (fun x => ↑(f x) • g x) μ
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<GOAL>(fun x => ↑(AEMeasurable.mk f hf x) • g x) =ᶠ[ae μ] fun x => ↑(f x) • g x
<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>E : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>g : α → E<VAR>x : α<VAR>hx : f x = AEMeasurable.mk f hf x<GOAL>↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Set β<GOAL>(SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Set β<VAR>ht : t.Subsingleton<GOAL>(SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>s t✝ : Set α<VAR>a b : α<VAR>f : α ↪ β<VAR>t : Set β<VAR>ht : t.Nontrivial<GOAL>(SimpleGraph.map f G).IsClique t ↔ t.Subsingleton ∨ ∃ s, G.IsClique s ∧ ⇑f '' s = t
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<GOAL>intrinsicInterior 𝕜 (⇑φ '' ∅) = ⇑φ '' intrinsicInterior 𝕜 ∅
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>W : Type u_3<VAR>Q : Type u_4<VAR>P : Type u_5<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : SeminormedAddCommGroup V<VAR>inst✝⁶ : SeminormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace 𝕜 V<VAR>inst✝⁴ : NormedSpace 𝕜 W<VAR>inst✝³ : MetricSpace P<VAR>inst✝² : PseudoMetricSpace Q<VAR>inst✝¹ : NormedAddTorsor V P<VAR>inst✝ : NormedAddTorsor W Q<VAR>φ : P →ᵃⁱ[𝕜] Q<VAR>s : Set P<VAR>hs : s.Nonempty<VAR>this✝ : Nonempty ↑s<VAR>f : ↥(affineSpan 𝕜 s) ≃ₜ ↥(map φ.toAffineMap (affineSpan 𝕜 s)) := (isometryEquivMap φ (affineSpan 𝕜 s)).toHomeomorph<VAR>this : ⇑φ.toAffineMap ∘ Subtype.val ∘ ⇑f.symm = Subtype.val<GOAL>intrinsicInterior 𝕜 (⇑φ '' s) = ⇑φ '' intrinsicInterior 𝕜 s
<VAR>J : Type v<VAR>inst✝² : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝¹ : IsFilteredOrEmpty J<VAR>inst✝ : HasColimit F<VAR>i j : J<VAR>xi : F.obj i<VAR>xj : F.obj j<GOAL>(equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨i, xi⟩) = (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨j, xj⟩) ↔ FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>p : α → Prop<VAR>x : α<VAR>hx : ¬p x<VAR>this : Fintype α<GOAL>Nat.card { x // p x } < Nat.card α
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<GOAL>∃ I, I.IsMaximal ∧ a ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<VAR>this : Ideal.span {a} ≠ ⊤<GOAL>∃ I, I.IsMaximal ∧ a ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<VAR>this : Ideal.span {a} ≠ ⊤<VAR>I : Ideal α<VAR>Imax : I.IsMaximal<VAR>H : Ideal.span {a} ≤ I<GOAL>∃ I, I.IsMaximal ∧ a ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<VAR>this : Ideal.span {a} ≠ ⊤<VAR>I : Ideal α<VAR>Imax : I.IsMaximal<VAR>H : Ideal.span {a} ≤ I<GOAL>a ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<VAR>this : Ideal.span {a} ≠ ⊤<VAR>I : Ideal α<VAR>Imax : I.IsMaximal<VAR>H : Ideal.span {a} ≤ I<GOAL>a ∈ Ideal.span {a}