ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>x✝² x✝¹ x✝ : ℤ<GOAL>(x✝² + x✝¹) * (x✝² - x✝¹) * x✝ ^ 2 = (x✝² + x✝) * (x✝² - x✝) * x✝¹ ^ 2 - (x✝¹ + x✝) * (x✝¹ - x✝) * x✝² ^ 2
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(vec ᵥ* adjMatrix α G) v = ∑ u ∈ G.neighborFinset v, vec u
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(vec ⬝ᵥ fun i => adjMatrix α G i v) = vec ⬝ᵥ adjMatrix α G v
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<GOAL>(fun i => adjMatrix α G i v) = adjMatrix α G v
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>G : SimpleGraph V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype V<VAR>inst✝ : NonAssocSemiring α<VAR>v : V<VAR>vec : V → α<VAR>x : V<GOAL>adjMatrix α G x v = adjMatrix α G v x
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : α<VAR>val✝¹ : List α<VAR>property✝ : val✝¹.length = n<VAR>val✝ : ℕ<VAR>isLt✝ : val✝ < n<GOAL>(set ⟨val✝¹, property✝⟩ ⟨val✝, isLt✝⟩ a).get ⟨val✝, isLt✝⟩ = a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>v : Fin n → R<VAR>i j : Fin n<GOAL>((vandermonde v)ᵀ * vandermonde v) i j = ∑ k : Fin n, v k ^ (↑i + ↑j)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>α : Type v<VAR>β : Type w<VAR>ι : Type u_6<VAR>M : Matrix m n α<VAR>i✝ : m<VAR>j✝ : n<VAR>b : n → α<VAR>c : m → α<VAR>inst✝¹ : DecidableEq l<VAR>inst✝ : DecidableEq m<VAR>A : Matrix m n α<VAR>i : l<VAR>r : o → α<VAR>e : l ≃ m<VAR>f : o ≃ n<VAR>i' : l<VAR>j : o<GOAL>(A.submatrix ⇑e ⇑f).updateRow i r i' j = (A.updateRow (e i) fun j => r (f.symm j)).submatrix (⇑e) (⇑f) i' j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>hb : 0 < b<GOAL>1 ≤ a / b ↔ b ≤ a
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>IsComplement S univ ↔ ∃ g, S = {g}
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : IsComplement S univ<GOAL>S.Nonempty
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : IsComplement S univ<VAR>a : G<VAR>ha : a ∈ S<VAR>b : G<VAR>hb : b ∈ S<GOAL>a = b
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<GOAL>(∃ g, S = {g}) → IsComplement S univ
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(pushout.inl f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.fst f g).op.unop
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>X✝ : Type v₂<VAR>X Y Z : C<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasPullback f g<VAR>inst✝ : HasPushout f.op g.op<GOAL>(pullbackIsoUnopPushout f g).hom ≫ (pushout.inl f.op g.op).unop = pullback.fst f g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v x < 1<GOAL>v (1 + x) = 1
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v x < v 1<GOAL>v (1 + x) = 1
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<GOAL>QuasispectrumRestricts a f ↔ SpectrumRestricts a f
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a ∪ {0}) ∧ Function.LeftInverse f ⇑(algebraMap R S) ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h : Function.LeftInverse f ⇑(algebraMap R S)<GOAL>Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a ∪ {0}) ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h' : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<VAR>x : S<VAR>hx : x ∈ spectrum S a ∪ {0}<GOAL>(algebraMap R S) (f x) = x
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>h : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h' : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)<VAR>x : S<VAR>hx : x = 0 ∨ x ∈ spectrum S a<GOAL>(algebraMap R S) (f x) = x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<VAR>x : K<GOAL>x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>frac : IsFractionRing R₁ K<VAR>inst✝ : IsDomain R₁<VAR>I✝ J✝ I J : FractionalIdeal R₁⁰ K<VAR>h : J ≠ 0<VAR>x : K<GOAL>x ∈ ⟨↑I / ↑J, ⋯⟩ ↔ ∀ y ∈ J, x * y ∈ I
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hA : schnirelmannDensity A = 0<GOAL>∃ n, 0 < n ∧ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n < ε
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hA : schnirelmannDensity A = 0<VAR>h : ∀ (n : ℕ), 0 < n → ε ≤ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n<GOAL>False
<VAR>A : Set ℕ<VAR>inst✝ : DecidablePred fun x => x ∈ A<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hA : schnirelmannDensity A = 0<VAR>h : ε ≤ schnirelmannDensity A<GOAL>False
<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✝ : F.PreservesRightHomologyOf S<GOAL>(S.map F).pOpcycles ≫ opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) = (S.map F).pOpcycles ≫ opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫ F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<GOAL>(eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) a = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<GOAL>(eval₂Hom (C.comp (Ideal.Quotient.mk I)) X) (∑ v ∈ a.support, (monomial v) (coeff v a)) = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<GOAL>∑ x ∈ a.support, eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial x) (coeff x a)) = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<VAR>n : σ →₀ ℕ<VAR>x✝ : n ∈ a.support<GOAL>eval₂ (C.comp (Ideal.Quotient.mk I)) X ((monomial n) (coeff n a)) = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<VAR>n : σ →₀ ℕ<VAR>x✝ : n ∈ a.support<GOAL>(C ((Ideal.Quotient.mk I) (coeff n a)) * n.prod fun n e => X n ^ e) = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<VAR>n : σ →₀ ℕ<VAR>x✝ : n ∈ a.support<GOAL>C ((Ideal.Quotient.mk I) (coeff n a)) = 0
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>I : Ideal R<VAR>a : MvPolynomial σ R<VAR>ha : a ∈ Ideal.map C I<VAR>n : σ →₀ ℕ<VAR>x✝ : n ∈ a.support<GOAL>coeff n a ∈ I
<VAR>M : Type u_1<VAR>inst✝⁶ : Monoid M<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : MulSemiringAction M R<VAR>S : Type u_3<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : MulSemiringAction M S<VAR>G : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : MulSemiringAction G S<VAR>g : G<VAR>f : S[X]<VAR>x : S<GOAL>eval (g • x) f = g • eval x (g⁻¹ • f)
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>(↑↑p).natAbs = (-↑p).natAbs
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>w.IsReal ∨ w.IsComplex
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>w.IsReal ∨ ¬w.IsReal
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y z : P<VAR>x : V<GOAL>midpoint R x (-x) = 0
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c x : α<VAR>u : αˣ<VAR>y : α<GOAL>x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a b c x : α<VAR>u : αˣ<VAR>y : α<GOAL>x = y * ↑u ↔ y * ↑u = x
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 ≤ z<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>(insert x s).einfsep ≤ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<GOAL>∀ i ∈ s, x ≠ i → (insert x s).einfsep ≤ edist x i
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<GOAL>Metric.ball 0 r₁ • p.closedBall 0 r₂ ⊆ p.ball 0 (r₁ * r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<GOAL>∀ (a : 𝕜), ‖a‖ < r₁ → ∀ (b : E), p b ≤ r₂ → ‖a‖ * p b < r₁ * r₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<VAR>a : 𝕜<VAR>ha : ‖a‖ < r₁<VAR>b : E<VAR>hb : p b ≤ r₂<GOAL>‖a‖ * p b < r₁ * r₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<VAR>a : 𝕜<VAR>ha : ‖a‖ < r₁<VAR>b : E<VAR>hb : p b ≤ r₂<GOAL>p b * ‖a‖ < r₂ * r₁
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁶ : SeminormedRing 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : SeminormedRing 𝕜₂<VAR>inst✝² : AddCommGroup E₂<VAR>inst✝¹ : Module 𝕜₂ E₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝ : RingHomIsometric σ₁₂<VAR>p✝ p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₂ : r₂ ≠ 0<VAR>a : 𝕜<VAR>ha : ‖a‖ < r₁<VAR>b : E<VAR>hb : p b ≤ r₂<GOAL>¬r₂ < 0
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, x ≤ 0<GOAL>sInf S ≤ 0
<VAR>hS : ∀ x ∈ ∅, x ≤ 0<GOAL>sInf ∅ ≤ 0
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, x ≤ 0<VAR>y : ℝ<VAR>hy : y ∈ S<GOAL>sInf S ≤ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f : Filter α<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>hf : Injective m<VAR>h : m '' s ∈ map m f<GOAL>s ∈ f
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : CanonicallyOrderedCommSemiring α<VAR>inst✝ : Nontrivial α<VAR>x : α<VAR>xs : List α<GOAL>0 < (x :: xs).prod ↔ ∀ x_1 ∈ x :: xs, 0 < x_1
<VAR>a : EReal<VAR>h : 0 ≤ a<GOAL>0 ≤ a⁻¹
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsSeparatedMap f<VAR>g : A → X<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>IsSeparatedMap (f ∘ g)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsClosed (Function.pullbackDiagonal f)<VAR>g : A → X<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>IsClosed (Function.pullbackDiagonal (f ∘ g))
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<VAR>sep : IsClosed (Function.pullbackDiagonal f)<VAR>g : A → X<VAR>cont : Continuous g<VAR>inj : Function.Injective g<GOAL>IsClosed (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝³ : Traversable t<VAR>inst✝² : LawfulTraversable t<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m α<VAR>x : β<GOAL>(⇑(foldlM.ofFreeMonoid f) ∘ FreeMonoid.of) x = (foldlM.mk ∘ flip f) x
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝³ : Traversable t<VAR>inst✝² : LawfulTraversable t<VAR>m : Type u → Type u<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m α<VAR>x : β<GOAL>(fun a => f a x) = fun a => f a x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : Algebra F R<VAR>inst✝² : Algebra F S<VAR>inst✝¹ : IsScalarTower F R S<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>f : S<VAR>hf : f ≠ 0<GOAL>Associated ((Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : Algebra F R<VAR>inst✝² : Algebra F S<VAR>inst✝¹ : IsScalarTower F R S<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>f : S<VAR>hf : f ≠ 0<VAR>hI : ¬span {f} = ⊥<GOAL>Associated ((Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : IsDomain R<VAR>inst✝⁸ : IsPrincipalIdealRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : IsDomain S<VAR>inst✝⁵ : Algebra R S<VAR>F : Type u_4<VAR>inst✝⁴ : CommRing F<VAR>inst✝³ : Algebra F R<VAR>inst✝² : Algebra F S<VAR>inst✝¹ : IsScalarTower F R S<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R S<VAR>f : S<VAR>hf : f ≠ 0<VAR>hI : ¬span {f} = ⊥<VAR>b' : Basis ι R S := ringBasis b (span {f}) hI<GOAL>Associated ((Algebra.norm R) f) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤)<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤)<VAR>pos : 0 < p<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>pos : 0 < p<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>pos : 0 < p<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<VAR>this : ↑((∑ i ∈ s, ((fun i => (f i).toNNReal) i + (fun i => (g i).toNNReal) i) ^ p) ^ (1 / p)) ≤ ↑((∑ i ∈ s, (fun i => (f i).toNNReal) i ^ p) ^ (1 / p) + (∑ i ∈ s, (fun i => (g i).toNNReal) i ^ p) ^ (1 / p))<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<VAR>pos : 0 < p<VAR>H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤<VAR>this : (∑ x ∈ s, (↑(f x).toNNReal + ↑(g x).toNNReal) ^ p) ^ (1 / p) ≤ (∑ x ∈ s, ↑(f x).toNNReal ^ p) ^ (1 / p) + (∑ x ∈ s, ↑(g x).toNNReal ^ p) ^ (1 / p)<GOAL>(∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a x : α<VAR>s t : List α<VAR>h : permutations'Aux x s = permutations'Aux x t<GOAL>s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a x : α<VAR>s t : List α<VAR>h : permutations'Aux x s = permutations'Aux x t<GOAL>insertNth s.length x s = insertNth s.length x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a x : α<VAR>s t : List α<VAR>h : permutations'Aux x s = permutations'Aux x t<VAR>hl : s.length = t.length<GOAL>insertNth s.length x s = insertNth s.length x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a x : α<VAR>s t : List α<VAR>h : permutations'Aux x s = permutations'Aux x t<VAR>hl : s.length = t.length<GOAL>(permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩
<VAR>f g : ℕ → ℂ<VAR>h : ∀ {n : ℕ}, n ≠ 0 → f n = g n<VAR>s : ℂ<VAR>n : ℕ<GOAL>term f s n = term g s n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : EnoughInjectives C<VAR>Z : C<GOAL>Injective.ι Z ≫ (ofCocomplex Z).d 0 1 = 0
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R✝ : Type u_1<VAR>inst✝¹ : CommSemiring R✝<VAR>a✝ a' a₁ a₂ a₃ b b' b₁ b₂ b₃ c c₁ c₂ : R✝<VAR>n : ℤ<VAR>d : ℕ<VAR>R : Type u_2<VAR>inst✝ : DivisionRing R<VAR>a : R<VAR>inv✝ : Invertible ↑d<VAR>e : a = ↑n * ⅟↑d<GOAL>a = Rat.rawCast n d + 0
<VAR>α : Type u<VAR>c✝ d : Cardinal.{u}<VAR>c : ℕ<GOAL>↑(toNat ↑c) = ↑c
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>M : HomologicalComplex C c<VAR>α : M ⟶ K<VAR>β : M ⟶ L<VAR>i : ι<GOAL>(biprod.lift α β).f i ≫ biprod.snd.f i = β.f i
<VAR>α : Sort u_1<VAR>n : Nat<VAR>f : α → Fin n → α<VAR>x : α<GOAL>foldr n (fun i x => f x i.rev) x = foldl n f x
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>e' : Cardinal.lift.{v, u} #α = (type s).card<GOAL>∃ a', lift.{v, u} a' = type s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>e' : Nonempty (α ≃ β)<GOAL>∃ a', lift.{v, u} a' = type s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a : Cardinal.{u}<VAR>b : Ordinal.{max u v}<VAR>h : b.card ≤ Cardinal.lift.{v, u} a<VAR>c : Cardinal.{u}<VAR>e : Cardinal.lift.{v, u} c = b.card<VAR>α : Type u<VAR>β : Type (max u v)<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<VAR>f : α ≃ β<VAR>g : ⇑f ⁻¹'o s ≃r s<GOAL>∃ a', lift.{v, u} a' = type s