ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<VAR>v : V<GOAL>(∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ x -ᵥ p i₀ = v) ↔ ∃ a, ∃ (_ : a ≠ i₀), p a -ᵥ p i₀ = v
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<GOAL>G.Connected ↔ ∃ v, ∀ (w : V), G.Reachable v w
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<GOAL>G.Preconnected ∧ Nonempty V ↔ ∃ v, ∀ (w : V), G.Reachable v w
<VAR>G : Type u_1<VAR>hG : Group G<VAR>inst✝ : Finite G<VAR>e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G<GOAL>Group.IsNilpotent G
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>map f (I ⊔ f.ker) = map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>map f (I ⊔ f.ker) ≤ map f I
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<GOAL>↑(Submodule.map (↑f) (lieIdealSubalgebra R L (I ⊔ f.ker)).toSubmodule) ⊆ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L'<VAR>y : L<VAR>hy₁ : y ∈ ↑(lieIdealSubalgebra R L (I ⊔ f.ker)).toSubmodule<VAR>hy₂ : ↑f y = x<GOAL>↑f y ∈ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L'<VAR>y : L<VAR>hy₁ : ∃ y_1 ∈ I, ∃ z ∈ f.ker, y_1 + z = y<VAR>hy₂ : ↑f y = x<GOAL>↑f y ∈ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L'<VAR>y : L<VAR>hy₂ : ↑f y = x<VAR>z₁ : L<VAR>hz₁ : z₁ ∈ I<VAR>z₂ : L<VAR>hz₂ : z₂ ∈ f.ker<VAR>hy : z₁ + z₂ = y<GOAL>↑f (z₁ + z₂) ∈ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L'<VAR>y : L<VAR>hy₂ : ↑f y = x<VAR>z₁ : L<VAR>hz₁ : z₁ ∈ I<VAR>z₂ : L<VAR>hz₂ : z₂ ∈ f.ker<VAR>hy : z₁ + z₂ = y<GOAL>f z₁ ∈ ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)
<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 : ℝ<VAR>x x✝ : E<GOAL>x✝ ∈ -p.ball x r ↔ x✝ ∈ p.ball (-x) r
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.20056, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.20063, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.20070, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>a : M<VAR>f : ShiftedHom X Y a<GOAL>a + m₀ = a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.20063, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.20070, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<VAR>a : M<VAR>f : ShiftedHom X Y a<GOAL>(mk₀ m₀ hm₀ (𝟙 X)).comp f ⋯ = f
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>preNormEDS' ((mapRingHom f) W.Ψ₂Sq ^ 2) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n = preNormEDS' ((mapRingHom f) (W.Ψ₂Sq ^ 2)) ((mapRingHom f) W.Ψ₃) ((mapRingHom f) W.preΨ₄) n
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>h : 0 < s.length<GOAL>x ∈ eraseLast s ↔ x ≠ last s ∧ x ∈ s
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s : CompositionSeries X<VAR>x : X<VAR>h : 0 < s.length<GOAL>(x ∈ range fun i => s.toFun ⟨↑i, ⋯⟩) ↔ x ≠ last s ∧ x ∈ range s.toFun
<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>s✝ : Finset α<VAR>H✝ : s✝.Nonempty<VAR>x a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsLeast (↑(insert a s)) (min (s.min' H) a)
<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>s✝ : Finset α<VAR>H✝ : s✝.Nonempty<VAR>x a : α<VAR>s : Finset α<VAR>H : s.Nonempty<GOAL>IsLeast (insert a ↑s) (min a (s.min' H))
<VAR>α : Type u_1<VAR>I : Type ?u.59101<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime x (y ^ n)
<VAR>α : Type u_1<VAR>I : Type ?u.59101<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecompositionMonoid α<VAR>x y z : α<VAR>s : I → α<VAR>t : Finset I<VAR>m n : ℕ<VAR>H : IsRelPrime x y<GOAL>IsRelPrime x (∏ _x ∈ Finset.range n, y)
<VAR>R✝ : Type u<VAR>inst✝⁹ : CommSemiring R✝<VAR>M✝ : Type v<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>ι : Type w<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>κ : Type u_1<VAR>inst✝⁴ : DecidableEq κ<VAR>inst✝³ : Fintype κ<VAR>b : Basis ι R✝ M✝<VAR>c : Basis κ R✝ M✝<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : Module.End R M<GOAL>(trace R M) ⁅f, g⁆ = 0
<VAR>R✝ : Type u<VAR>inst✝⁹ : CommSemiring R✝<VAR>M✝ : Type v<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>ι : Type w<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : Fintype ι<VAR>κ : Type u_1<VAR>inst✝⁴ : DecidableEq κ<VAR>inst✝³ : Fintype κ<VAR>b : Basis ι R✝ M✝<VAR>c : Basis κ R✝ M✝<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : Module.End R M<GOAL>(trace R M) (g * f) - (trace R M) (g * f) = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : NoZeroDivisors R<VAR>ζ : R<VAR>h : IsPrimitiveRoot ζ 2<GOAL>ζ = -1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : NoZeroDivisors R<VAR>ζ : R<VAR>h : IsPrimitiveRoot ζ 2<GOAL>¬ζ = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : NoZeroDivisors R<VAR>ζ : R<VAR>h : IsPrimitiveRoot ζ 2<GOAL>ζ ^ 2 = 1 ^ 2
<VAR>s : Finset ℕ<VAR>m n : ℕ<VAR>hm : m ∈ factoredNumbers s<VAR>hn : n ∈ factoredNumbers s<GOAL>m * n ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>m n : ℕ<VAR>hm : m ∈ factoredNumbers s<VAR>hn : n ∈ factoredNumbers s<VAR>hm' : m.primeFactors ⊆ s<GOAL>m * n ∈ factoredNumbers s
<VAR>s : Finset ℕ<VAR>m n : ℕ<VAR>hm : m ∈ factoredNumbers s<VAR>hn : n ∈ factoredNumbers s<VAR>hm' : m.primeFactors ⊆ s<VAR>hn' : n.primeFactors ⊆ s<GOAL>m * n ∈ factoredNumbers s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card ≤ s.card / P.parts.card + 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<VAR>P : Finpartition s<VAR>hP : P.IsEquipartition<VAR>ht : t ∈ P.parts<GOAL>t.card ≤ (∑ i ∈ P.parts, i.card) / P.parts.card + 1
<VAR>ι : Type u_1<VAR>m✝ : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝⁵ : Fintype m✝<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype p<VAR>inst✝² : AddCommMonoid R<VAR>inst✝¹ : DecidableEq p<VAR>m : p → Type u_8<VAR>inst✝ : (i : p) → Fintype (m i)<VAR>M : (i : p) → Matrix (m i) (m i) R<GOAL>(blockDiagonal' M).trace = ∑ i : p, (M i).trace
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>n : ℤ<GOAL>x ^ (y * ↑n) = (x ^ y) ^ n
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => |(f' x).det|) (μ.restrict s)
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<GOAL>AEMeasurable (fun x => (f' x).det) (μ.restrict s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝¹ : Semifield R<VAR>inst✝ : StarRing R<VAR>x y : R<VAR>hx : IsSelfAdjoint x<VAR>hy : IsSelfAdjoint y<GOAL>IsSelfAdjoint (x / y)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>β : Sort u_1<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝⁶ : Category.{u_4, u_3} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroObject C<VAR>K L M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>inst✝³ : e.IsTruncGE<VAR>inst✝² : ∀ (i' : ι'), K.HasHomology i'<VAR>inst✝¹ : ∀ (i' : ι'), L.HasHomology i'<VAR>inst✝ : ∀ (i' : ι'), M.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : e.BoundaryGE i<GOAL>(if hij : c.Rel i j then if hi : e.BoundaryGE i then (truncGE'.XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv else (truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv else 0) = (K.truncGE'XIsoOpcycles e hi' hi).hom ≫ K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>c : ComplexShape ι<VAR>c' : ComplexShape ι'<VAR>C : Type u_3<VAR>inst✝⁶ : Category.{u_4, u_3} C<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroObject C<VAR>K L M : HomologicalComplex C c'<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>e : c.Embedding c'<VAR>inst✝³ : e.IsTruncGE<VAR>inst✝² : ∀ (i' : ι'), K.HasHomology i'<VAR>inst✝¹ : ∀ (i' : ι'), L.HasHomology i'<VAR>inst✝ : ∀ (i' : ι'), M.HasHomology i'<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>i' j' : ι'<VAR>hi' : e.f i = i'<VAR>hj' : e.f j = j'<VAR>hi : e.BoundaryGE i<GOAL>(truncGE'.XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv = (K.truncGE'XIsoOpcycles e hi' hi).hom ≫ K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<GOAL>𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>a : A<GOAL>r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>e : (a :: l).length = n.succ<VAR>i : ℕ<VAR>h : i < n<GOAL>(tail ⟨a :: l, e⟩).get ⟨i, h⟩ = get ⟨a :: l, e⟩ ⟨i, h⟩.succ
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>e : (a :: l).length = n.succ<VAR>i : ℕ<VAR>h : i < n<GOAL>(tail ⟨a :: l, e⟩).toList[i] = l[i]
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ i : ι, f i
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : ι → α<GOAL>∏ j : κ, ∏ i : { i // g i = j }, f ↑i = ∏ j : κ, ∏ i ∈ filter (fun i => g i = j) univ, f i
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : ι → α<VAR>j : κ<GOAL>∏ i : { i // g i = j }, f ↑i = ∏ i ∈ filter (fun i => g i = j) univ, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : f₁ =O[l] g<VAR>h₂ : f₂ =O[l] g<GOAL>(fun x => f₁ x - f₂ x) =O[l] g
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>Nat.card (↥H.normalizer ⧸ comap H.normalizer.subtype H) ≡ Nat.card (G ⧸ H) [MOD p]
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>H : Subgroup G<VAR>hH : Nat.card ↥H = p ^ n<GOAL>Nat.card ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≡ Nat.card (G ⧸ H) [MOD p]
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>f : V ↪ W<VAR>G : SimpleGraph W<GOAL>SimpleGraph.map f (SimpleGraph.comap (⇑f) G) ≤ G
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedField α<VAR>inst✝ : FloorRing α<GOAL>round 2⁻¹ = 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x ≤ y<GOAL>TransGen (fun x x_1 => x ⩿ x_1) x y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>x y : α<VAR>hxy : x ≤ y<VAR>this : (Ico x y).card < (Icc x y).card<GOAL>TransGen (fun x x_1 => x ⩿ x_1) x y
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x✝ y✝ : α<VAR>Φ : α → β<VAR>h : IsCompact s<VAR>hne : s.Nonempty<VAR>x y : α<VAR>hys : y ∈ s<VAR>hy : infEdist x s = edist x y<GOAL>infDist x s = dist x y
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<GOAL>ifp_succ_n.fr.num < ifp_n.fr.num
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<VAR>ifp_n' : IntFractPair ℚ<VAR>stream_nth_eq' : IntFractPair.stream q n = some ifp_n'<VAR>ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0<VAR>IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n<GOAL>ifp_succ_n.fr.num < ifp_n.fr.num
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<VAR>ifp_n' : IntFractPair ℚ<VAR>stream_nth_eq' : IntFractPair.stream q n = some ifp_n'<VAR>ifp_n_fract_ne_zero : ifp_n'.fr ≠ 0<VAR>IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n'.fr⁻¹ = ifp_succ_n<VAR>this : ifp_n = ifp_n'<GOAL>ifp_succ_n.fr.num < ifp_n.fr.num
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<VAR>stream_nth_eq' : IntFractPair.stream q n = some ifp_n<VAR>ifp_n_fract_ne_zero : ifp_n.fr ≠ 0<VAR>IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<GOAL>(IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<VAR>stream_nth_eq' : IntFractPair.stream q n = some ifp_n<VAR>ifp_n_fract_ne_zero : ifp_n.fr ≠ 0<VAR>IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>zero_le_ifp_n_fract : 0 ≤ ifp_n.fr<VAR>ifp_n_fract_lt_one : ifp_n.fr < 1<GOAL>(IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>q : ℚ<VAR>n : ℕ<VAR>ifp_n ifp_succ_n : IntFractPair ℚ<VAR>stream_nth_eq : IntFractPair.stream q n = some ifp_n<VAR>stream_succ_nth_eq : IntFractPair.stream q (n + 1) = some ifp_succ_n<VAR>stream_nth_eq' : IntFractPair.stream q n = some ifp_n<VAR>ifp_n_fract_ne_zero : ifp_n.fr ≠ 0<VAR>IntFractPair.of_eq_ifp_succ_n : IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n<VAR>zero_le_ifp_n_fract : 0 ≤ ifp_n.fr<VAR>ifp_n_fract_lt_one : ifp_n.fr < 1<VAR>this : 0 < ifp_n.fr<GOAL>(IntFractPair.of ifp_n.fr⁻¹).fr.num < ifp_n.fr.num
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>g : SpecialLinearGroup n R<GOAL>(f.mapMatrix ↑g).det = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>g : SpecialLinearGroup n R<GOAL>f (↑g).det = 1
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ s<GOAL>∃ t ∈ P.parts, a ∈ t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ha : a ∈ P.parts.sup id<GOAL>∃ t ∈ P.parts, a ∈ t
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>t : Set (α × α)<GOAL>⋂ V ∈ 𝓤 α, V ○ t ○ V = ⋂ V ∈ 𝓤 α, V ○ (t ○ V)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i<VAR>h0 : p 0 = 0<VAR>n : ℕ<VAR>v : Fin n → F<GOAL>(p.comp (p.rightInv i) n) v = (id 𝕜 F n) v