ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>h₂ : IsZero T.obj₂<VAR>h₃ : IsZero T.obj₃<GOAL>T.mor₁ = 0 ∧ T.mor₃ = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c d : α<GOAL>Ico a b ∩ Ico c d = Ico (max a c) (min b d)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<GOAL>Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<GOAL>Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<GOAL>Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<VAR>e₂ : (X.restrictFunctor.obj V).left.presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.restrictFunctor.map i).left (V.ι ⁻¹ᵁ V.ι ''ᵁ W) = Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op<GOAL>Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<VAR>e₂ : (X.restrictFunctor.obj V).left.presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.restrictFunctor.map i).left (V.ι ⁻¹ᵁ V.ι ''ᵁ W) = Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op<VAR>e₃ : Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<GOAL>Hom.app (X.restrictFunctor.map i).left W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<VAR>e₂ : (X.restrictFunctor.obj V).left.presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.restrictFunctor.map i).left (V.ι ⁻¹ᵁ V.ι ''ᵁ W) = Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op<VAR>e₃ : Hom.app (IsOpenImmersion.lift V.ι U.ι ⋯) W ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map ((Opens.map (IsOpenImmersion.lift V.ι U.ι ⋯).val.base).map (eqToHom this))).op = X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op<GOAL>Hom.app (IsOpenImmersion.lift V.ι U.ι ⋯) W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<VAR>e₂ : (X.restrictFunctor.obj V).left.presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.restrictFunctor.map i).left (V.ι ⁻¹ᵁ V.ι ''ᵁ W) = Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op<VAR>e₃ : Hom.app (IsOpenImmersion.lift V.ι U.ι ⋯) W = X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫ X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (IsOpenImmersion.lift V.ι U.ι ⋯).val.base).map (eqToHom this))).op)<GOAL>Hom.app (IsOpenImmersion.lift V.ι U.ι ⋯) W = X.presheaf.map (homOfLE ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U✝ U V : X.Opens<VAR>i : U ⟶ V<VAR>W : (↑V).Opens<VAR>e₁ : Hom.app ((X.restrictFunctor.map i).left ≫ V.ι) (V.ι ''ᵁ W) = Hom.app U.ι (V.ι ''ᵁ W) ≫ (X.restrictFunctor.obj U).left.presheaf.map (eqToHom ⋯).op<VAR>this : V.ι ⁻¹ᵁ V.ι ''ᵁ W = W<VAR>e₂ : (X.restrictFunctor.obj V).left.presheaf.map (eqToIso this).hom.op ≫ Hom.app (X.restrictFunctor.map i).left (V.ι ⁻¹ᵁ V.ι ''ᵁ W) = Hom.app (X.restrictFunctor.map i).left W ≫ (X.restrictFunctor.obj U).left.presheaf.map ((Opens.map (X.restrictFunctor.map i).left.val.base).map (eqToIso this).hom.op.unop).op<VAR>e₃ : Hom.app (IsOpenImmersion.lift V.ι U.ι ⋯) W = X.presheaf.map ((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫ X.presheaf.map (inv ((Hom.opensFunctor U.ι).map ((Opens.map (IsOpenImmersion.lift V.ι U.ι ⋯).val.base).map (eqToHom this))).op)<GOAL>X.presheaf.map (((homOfLE ⋯).op ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) ≫ inv ((Hom.opensFunctor U.ι).map ((Opens.map (IsOpenImmersion.lift V.ι U.ι ⋯).val.base).map (eqToHom this))).op) = X.presheaf.map (homOfLE ⋯).op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : ℕ × α<VAR>l : List α<VAR>h : x ∈ l.enum<GOAL>x.1 < l.length
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<GOAL>p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 2 = 1<GOAL>p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 8 % 2 = 1<GOAL>p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hp : p ≠ 2<VAR>h₁ : p % 8 % 2 = 1<VAR>h₂ : p % 8 < 8<GOAL>p % 8 ≠ 5 ∧ p % 8 ≠ 7 ↔ p % 8 = 1 ∨ p % 8 = 3
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>IsCompl ↑I ↑(orthogonal Φ hΦ_inv I)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module K M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : Module.Finite K L<VAR>Φ : LinearMap.BilinForm K L<VAR>hΦ_nondeg : Φ.Nondegenerate<VAR>hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ<VAR>hΦ_refl : Φ.IsRefl<VAR>hL : ∀ (I : LieIdeal K L), IsAtom I → ¬IsLieAbelian ↥↑I<VAR>I : LieIdeal K L<VAR>hI : IsAtom I<GOAL>Disjoint I (orthogonal Φ hΦ_inv I)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<VAR>f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<VAR>f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)<VAR>hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<VAR>f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)<VAR>hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x<VAR>hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<VAR>f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)<VAR>hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x<VAR>hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s<VAR>g : E × ℝ →ₗ[ℝ] ℝ<VAR>g_eq : ∀ (x : ↥f'.domain), g ↑x = ↑f' x<VAR>g_nonneg : ∀ x ∈ s, 0 ≤ g x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>N : E → ℝ<VAR>N_hom : ∀ (c : ℝ), 0 < c → ∀ (x : E), N (c • x) = c * N x<VAR>N_add : ∀ (x y : E), N (x + y) ≤ N x + N y<VAR>hf : ∀ (x : ↥f.domain), ↑f x ≤ N ↑x<VAR>s : ConvexCone ℝ (E × ℝ) := { carrier := {p | N p.1 ≤ p.2}, smul_mem' := ⋯, add_mem' := ⋯ }<VAR>f' : E × ℝ →ₗ.[ℝ] ℝ := (-f).coprod (LinearMap.id.toPMap ⊤)<VAR>hf'_nonneg : ∀ (x : ↥f'.domain), ↑x ∈ s → 0 ≤ ↑f' x<VAR>hf'_dense : ∀ (y : E × ℝ), ∃ x, ↑x + y ∈ s<VAR>g : E × ℝ →ₗ[ℝ] ℝ<VAR>g_nonneg : ∀ x ∈ s, 0 ≤ g x<VAR>g_eq : ∀ (x : ↥f.domain) (y : ℝ), g (↑x, y) = y - ↑f x<GOAL>∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ (x : E), g x ≤ N x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasRightHomology<VAR>inst✝² : S₂.HasRightHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>F.map (rightHomologyMap φ) ≫ (S₂.mapRightHomologyIso F).inv = (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosSemidef<VAR>x : m → R<GOAL>0 ≤ star x ⬝ᵥ (A + B) *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A B : Matrix m m R<VAR>hA : A.PosSemidef<VAR>hB : B.PosSemidef<VAR>x : m → R<GOAL>0 ≤ star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x
<VAR>a₁ a₂ b : ℕ<VAR>h : a₁ < a₂<GOAL>pair a₁ b < pair a₂ b
<VAR>a₁ a₂ b : ℕ<VAR>h : a₁ < a₂<VAR>h₁ : a₁ < b<GOAL>b * b + a₁ < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
<VAR>a₁ a₂ b : ℕ<VAR>h : a₁ < a₂<VAR>h₁ : ¬a₁ < b<GOAL>a₁ * a₁ + (a₁ + b) < if a₂ < b then b * b + a₂ else a₂ * a₂ + (a₂ + b)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>g f : K[X]<VAR>hf0 : g * f ≠ 0<VAR>hf : Splits i (g * f)<GOAL>Splits i g
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<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✝⁸ : 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>v : V<VAR>x✝ : P<GOAL>x✝ ∈ v +ᵥ ⊤ ↔ x✝ ∈ ⊤
<VAR>z : ℂ<GOAL>-(z * I) * I = z
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 2)<VAR>j : Fin (n + 1)<VAR>H : j.castSucc < i<GOAL>X.map (SimplexCategory.σ j.castSucc).op ≫ X.map (SimplexCategory.δ i.succ).op = X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>s : Multiset α<VAR>inst✝ : Std.Commutative op<VAR>a : α<GOAL>noncommFold op s ⋯ a = fold op a s
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>assoc : Std.Associative op<VAR>inst✝ : Std.Commutative op<VAR>a : α<VAR>a✝ : List α<GOAL>noncommFold op ⟦a✝⟧ ⋯ a = fold op a ⟦a✝⟧
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>Gamma s = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>(↑s).GammaIntegral.re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>(∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (↑s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>(∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1)).re = ∫ (x : ℝ) in Ioi 0, rexp (-x) * x ^ (s - 1)
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x) * x ^ (s - 1))
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>↑(rexp (-x)) * ↑x ^ ↑(s - 1) = ↑(rexp (-x) * x ^ (s - 1))
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑(x ^ (s - 1))
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>Complex.exp (-↑x) * ↑x ^ (↑s - 1) = Complex.exp (-↑x) * ↑x ^ ↑(s - 1)
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>hf : AnalyticAt 𝕜 f z₀<VAR>hg : AnalyticAt 𝕜 g z₀<GOAL>(∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = g z) ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = g z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<GOAL>∀ t ∈ {∅}, MeasurableSet t
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : IsNormal (f i)<VAR>a : Ordinal.{max u v}<GOAL>f i (sup (List.foldr f a)) = sup (List.foldr f a)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : IsNormal (f i)<VAR>a : Ordinal.{max u v}<GOAL>sup (f i ∘ List.foldr f a) = sup (List.foldr f a)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>l : List ι<GOAL>(f i ∘ List.foldr f a) l ≤ sup (List.foldr f a)
<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>i : ι<VAR>H : IsNormal (f i)<VAR>a : Ordinal.{max u v}<VAR>l : List ι<GOAL>List.foldr f a l ≤ sup (f i ∘ List.foldr f a)
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<GOAL>a * b ≤ max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<GOAL>max a b = max a b * max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<GOAL>ℵ₀ ≤ max a b
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<GOAL>∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i = (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<VAR>A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) = ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i<GOAL>∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i = (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>R : Type u_3<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : NonAssocSemiring R<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>f : ℕ → ℕ → M<VAR>n : ℕ<VAR>A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) = ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i<GOAL>(∏ k ∈ range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ (n + 1).choose (k + 1)) * f 0 (n + 1 - 0) ^ (n + 1).choose 0 = (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i) * ∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β → F<VAR>s : Set β<VAR>hf : ∀ (i : α), ContinuousOn (f i) s<VAR>hu : Summable u<VAR>hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n<GOAL>ContinuousOn (fun x => ∑' (n : α), f n x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH1 : (ts.permutationsAux (t :: is)).length + (t :: is).length ! = (ts.length + (t :: is).length)!<VAR>IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!<VAR>IH2 : (is.permutationsAux []).length + 1 = is.length !<GOAL>((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a t : α<VAR>ts is : List α<VAR>IH2✝ : (is.permutationsAux []).length + [].length ! = (is.length + [].length)!<VAR>IH2 : (is.permutationsAux []).length + 1 = is.length !<VAR>IH1 : (ts.permutationsAux (t :: is)).length + is.length ! * is.length.succ = (ts.length + is.length)! * (ts.length + is.length).succ<GOAL>((t :: ts).permutationsAux is).length + is.length ! = ((t :: ts).length + is.length)!
<VAR>R : Type uR<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>ψ : Dual R M₂<GOAL>f.dualMap ψ ∈ (ker f).dualAnnihilator
<VAR>R : Type uR<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>ψ : Dual R M₂<GOAL>∀ (w : M₁), f w = 0 → (f.dualMap ψ) w = 0
<VAR>R : Type uR<VAR>inst✝⁴ : CommSemiring R<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>f : M₁ →ₗ[R] M₂<VAR>ψ : Dual R M₂<VAR>x : M₁<VAR>hx : f x = 0<GOAL>(f.dualMap ψ) x = 0
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B✝ : Matrix n n α<VAR>B : Matrix n m α<VAR>h : IsUnit A.det<GOAL>A * (A⁻¹ * B) = B
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>s : (i : κ) → κ' i → HomogeneousIdeal 𝒜<GOAL>(⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : u n ≤ x<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x : α<VAR>hx : x ∈ s<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<VAR>n : ℕ<VAR>h : x < u n<VAR>exists_N : ∃ N ≤ n, x < u N<VAR>N : ℕ := Nat.find exists_N<GOAL>∃ v m, Monotone v ∧ (∀ (i : ℕ), v i ∈ s) ∧ x ∈ v '' Iio m ∧ ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) ≤ ∑ j ∈ Finset.range m, edist (f (v (j + 1))) (f (v j))