ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : LinearOrder α✝<VAR>inst✝² : OrderBot α✝<VAR>s✝ : Finset ι<VAR>f✝ : ι → α✝<VAR>a : α✝<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : BoundedOrder α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : LinearOrder α✝<VAR>inst✝² : OrderBot α✝<VAR>s✝ : Finset ι<VAR>f✝ : ι → α✝<VAR>a : α✝<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : BoundedOrder α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<VAR>h✝ : Subsingleton α<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝³ : LinearOrder α✝<VAR>inst✝² : OrderBot α✝<VAR>s✝ : Finset ι<VAR>f✝ : ι → α✝<VAR>a : α✝<VAR>α : Type u_7<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : BoundedOrder α<VAR>s : Finset ι<VAR>f : ι → α<VAR>hs : s.Nonempty<VAR>h✝ : Nontrivial α<GOAL>s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>M N : PresheafOfModules R<VAR>φ : M ⟶ N<VAR>x : ↑((evaluation R X).obj M)<GOAL>((evaluation R X).map φ ≫ restrictionApp f N) x = (restrictionApp f M ≫ (evaluation R Y ⋙ ModuleCat.restrictScalars (R.map f)).map φ) x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>h : a⁻¹ ∈ s<GOAL>a ∈ s
<VAR>x : ℂ<GOAL>|(x ^ 2⁻¹).im| = √((abs x - x.re) / 2)
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>a : M<VAR>b : CliffordAlgebra Q<GOAL>(contractRight (b * (ι Q) a)) d = d a • b - (contractRight b) d * (ι Q) a
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<GOAL>μ s ≤ (μ.toMeasure ⋯) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalGroup α<VAR>f g : β → α<VAR>a a₁ a₂ : α<VAR>hfg : Multipliable fun b => f b / g b<VAR>hf : Multipliable f<GOAL>Multipliable fun b => g b / f b
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>↑x = 0 ↔ ∃ n, n • p = x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝² : LinearOrderedAddCommGroup 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : 0 < p<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>(∃ n, n • p = x) ↔ ∃ n, n • p = x
<VAR>α : Type u<VAR>β : α → Type v<GOAL>#((a : α) × (β a → WType β)) = sum fun a => #(WType β) ^ lift.{u, v} #(β a)
<VAR>α : Type u<VAR>β : α → Type v<GOAL>(sum fun i => lift.{v, max u v} #(WType β) ^ lift.{max u v, v} #(β i)) = sum fun a => #(WType β) ^ lift.{u, v} #(β a)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ ⟪x, y⟫_ℝ = 0
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h0 : 0 ≤ InnerProductGeometry.angle x y<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h0 : 0 ≤ InnerProductGeometry.angle x y<VAR>hpi : InnerProductGeometry.angle x y ≤ π<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h0 : 0 ≤ InnerProductGeometry.angle x y<VAR>hpi : InnerProductGeometry.angle x y ≤ π<VAR>h : o.oangle x y = ↑(InnerProductGeometry.angle x y)<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h0 : 0 ≤ InnerProductGeometry.angle x y<VAR>hpi : InnerProductGeometry.angle x y ≤ π<VAR>h : o.oangle x y = -↑(InnerProductGeometry.angle x y)<GOAL>InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : M.charpoly • 1 = M.charmatrix.adjugate * M.charmatrix<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv (M.charmatrix.adjugate * M.charmatrix)<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : matPolyEquiv (M.charpoly • 1) = matPolyEquiv M.charmatrix.adjugate * (X - C M)<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : eval M (matPolyEquiv (M.charpoly • 1)) = eval M (matPolyEquiv M.charmatrix.adjugate * (X - C M))<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : eval M (matPolyEquiv (M.charpoly • 1)) = 0<GOAL>(aeval M) M.charpoly = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : Fintype n<VAR>M₁₁ : Matrix m m R<VAR>M₁₂ : Matrix m n R<VAR>M₂₁ : Matrix n m R<VAR>M₂₂ M✝ : Matrix n n R<VAR>i j : n<VAR>M : Matrix n n R<VAR>h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0<GOAL>(aeval M) M.charpoly = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (quasiIso C c).HasLocalization<VAR>i : ι<VAR>x✝² x✝¹ : HomologicalComplex C c<VAR>x✝ : x✝² ⟶ x✝¹<VAR>hf : quasiIso C c x✝<GOAL>IsIso ((homologyFunctor C c i).map x✝)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : CategoryWithHomology C<VAR>inst✝ : (quasiIso C c).HasLocalization<VAR>i : ι<VAR>x✝² x✝¹ : HomologicalComplex C c<VAR>x✝ : x✝² ⟶ x✝¹<VAR>hf : QuasiIso x✝<GOAL>IsIso ((homologyFunctor C c i).map x✝)
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<GOAL>Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<GOAL>Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<GOAL>Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<GOAL>(Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<VAR>hsep' : IsSeparable E x<GOAL>(Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<VAR>hsep' : IsSeparable E x<VAR>this : Algebra.IsSeparable F ↥F⟮x⟯<GOAL>(Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<VAR>hsep' : IsSeparable E x<VAR>this✝ : Algebra.IsSeparable F ↥F⟮x⟯<VAR>this : Algebra.IsSeparable E ↥E⟮x⟯<GOAL>(Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
<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>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>x : K<VAR>hsep : IsSeparable F x<VAR>inst✝ : IsPurelyInseparable F E<VAR>hi : IsIntegral F x<VAR>hi' : IsIntegral E x<VAR>hsep' : IsSeparable E x<VAR>this✝² : Algebra.IsSeparable F ↥F⟮x⟯<VAR>this✝¹ : Algebra.IsSeparable E ↥E⟮x⟯<VAR>this✝ : Algebra.IsAlgebraic F ↥F⟮x⟯<VAR>this : Algebra.IsAlgebraic E ↥E⟮x⟯<GOAL>(Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t x : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x_le : x ≤ t<GOAL>t.truncateToReal x = x.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t x : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x_le : x ≤ t<VAR>x_lt_top : x < ⊤<GOAL>t.truncateToReal x = x.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>t x : ℝ≥0∞<VAR>t_ne_top : t ≠ ⊤<VAR>x_le : x ≤ t<VAR>x_lt_top : x < ⊤<VAR>obs : min t x ≠ ⊤<GOAL>t.truncateToReal x = x.toReal
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(freeOn E).Base B ↔ B = E
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>x : ((i : ι) → Ms i) ⧸ pi Set.univ p<VAR>x' : (i : ι) → Ms i<GOAL>invFun p (toFun p (Quotient.mk'' x')) = Quotient.mk'' x'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>x : ((i : ι) → Ms i) ⧸ pi Set.univ p<VAR>x' : (i : ι) → Ms i<GOAL>invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁸ : CommRing R<VAR>Ms : ι → Type u_3<VAR>inst✝⁷ : (i : ι) → AddCommGroup (Ms i)<VAR>inst✝⁶ : (i : ι) → Module R (Ms i)<VAR>N : Type u_4<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>Ns : ι → Type u_5<VAR>inst✝³ : (i : ι) → AddCommGroup (Ns i)<VAR>inst✝² : (i : ι) → Module R (Ns i)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>p : (i : ι) → Submodule R (Ms i)<VAR>x : ((i : ι) → Ms i) ⧸ pi Set.univ p<VAR>x' : (i : ι) → Ms i<GOAL>(piQuotientLift p (pi Set.univ p) single ⋯) ((quotientPiLift p (fun i => (p i).mkQ) ⋯) (Quotient.mk x')) = Quotient.mk x'
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M : Type x<VAR>inst✝³ : Monoid M<VAR>φ : G →* H<VAR>A B C : Type u<VAR>inst✝² : CommGroup A<VAR>inst✝¹ : CommGroup B<VAR>inst✝ : CommGroup C<VAR>f : A →* B<VAR>g : B →* A<VAR>e : A ≃* B<VAR>d : B ≃* C<VAR>n : ℤ<VAR>x : A ⧸ (zpowGroupHom n).range<GOAL>(MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) x = (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) x
<VAR>G : Type u<VAR>inst✝⁵ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝⁴ : Group H<VAR>M : Type x<VAR>inst✝³ : Monoid M<VAR>φ : G →* H<VAR>A B C : Type u<VAR>inst✝² : CommGroup A<VAR>inst✝¹ : CommGroup B<VAR>inst✝ : CommGroup C<VAR>f : A →* B<VAR>g : B →* A<VAR>e : A ≃* B<VAR>d : B ≃* C<VAR>n : ℤ<VAR>x : A ⧸ (zpowGroupHom n).range<GOAL>(MulEquiv.refl (A ⧸ (zpowGroupHom n).range)) (Quotient.mk'' (Quotient.out' x)) = (equivQuotientZPowOfEquiv (MulEquiv.refl A) n) (Quotient.mk'' (Quotient.out' x))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>hv : v ∈ Kᗮ<GOAL>↑((orthogonalProjection K) v) = ↑0
<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>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'<GOAL>l = l'
<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>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'<GOAL>l ≤ l'
<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>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p' s'<VAR>h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i<VAR>h' : ∀ (i' : ι'), p' i' → ∃ i, p i ∧ s i ⊆ s' i'<GOAL>l' ≤ l
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.num ≠ 0<GOAL>↑(q / r) = ↑q / ↑r
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.num ≠ 0<GOAL>↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>hq : ↑q.den ≠ 0<VAR>hr : ↑r.num ≠ 0<GOAL>↑(q.den * r.num) ≠ 0
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>(α_ X (𝟙_ C) Y).inv ≫ (ρ_ X).hom ▷ Y = X ◁ (λ_ Y).hom
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<GOAL>⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r • x = 0}
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<GOAL>⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r ∈ (Submodule.span R {x}).annihilator}
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<GOAL>∀ i ∈ associatedPrimes R M, ↑i ⊆ {r | ∃ x, x ≠ 0 ∧ r ∈ (Submodule.span R {x}).annihilator}
<VAR>R : Type u_1<VAR>inst✝⁵ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>M' : Type u_3<VAR>inst✝² : AddCommGroup M'<VAR>inst✝¹ : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsNoetherianRing R<GOAL>{r | ∃ x, x ≠ 0 ∧ r ∈ (Submodule.span R {x}).annihilator} ⊆ ⋃ p ∈ associatedPrimes R M, ↑p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : IsOpenMap f<VAR>s : Set Y<GOAL>f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M✝ : Type u_5<VAR>N : Type u_6<VAR>inst✝² : CommMonoid M✝<VAR>inst✝¹ : CommMonoid N<VAR>f✝ g : α → M✝<VAR>a b : α<VAR>s t : Set α<VAR>M : Type u_7<VAR>inst✝ : OrderedCommMonoid M<VAR>i : α<VAR>f : α → M<VAR>hf : (mulSupport f).Finite<VAR>h : ∀ (j : α), 1 ≤ f j<GOAL>f i ≤ ∏ᶠ (j : α), f j
<VAR>α : Type u_1<VAR>inst✝³ : CompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<GOAL>sInf (s / t) = sInf s / sSup t
<VAR>d : ℤ<VAR>a : Solution₁ d<GOAL>a = 1 ∨ a = -1 ↔ a.y = 0
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>H : a.y = 0<GOAL>a = 1 ∨ a = -1
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>H : a.y = 0<VAR>prop : a.x ^ 2 - d * a.y ^ 2 = 1<GOAL>a = 1 ∨ a = -1
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>H : a.y = 0<VAR>prop : a.x = 1 ∨ a.x = -1<GOAL>a = 1 ∨ a = -1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : ker f = ⊥<VAR>p p' : Submodule R M<GOAL>map f p ≤ map f p' ↔ p ≤ p'
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<GOAL>x = ↑x.valMinAbs ∧ x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>x.valMinAbs = y
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>x.valMinAbs - y = 0
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>↑n ∣ x.valMinAbs - y
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>|x.valMinAbs - y| < ↑n
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>|x.valMinAbs - y| * 2 < ↑n * 2
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>|x.valMinAbs - y| * |2| < ↑n * 2
<VAR>m n✝ n : ℕ<VAR>inst✝ : NeZero n<VAR>x : ZMod n<VAR>y : ℤ<VAR>h : x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n<GOAL>-(↑n * 2) < x.valMinAbs * 2 - y * 2 ∧ x.valMinAbs * 2 - y * 2 < ↑n * 2
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.areaForm x) y = -(o.areaForm y) x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>o.volumeForm ![x, y] = -o.volumeForm ![y, x]
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>![x, y] = ![y, x] ∘ ⇑(Equiv.swap 0 1)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>0 ≠ 1
<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>α : Type u_4<VAR>inst✝¹ : Fintype α<VAR>inst✝ : IsEmpty α<VAR>β : α → Type u_5<VAR>m : (α : α) → MeasurableSpace (β α)<VAR>μ : (a : α) → Measure (β a)<GOAL>(Measure.pi μ) univ = 1
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<GOAL>e ∈ (G.replaceVertex s t).edgeSet ↔ e ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}