ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x + y‖ = ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x + y‖ = ‖x‖ + ‖y‖<VAR>hxy₁ : 0 ≤ ‖x + y‖<VAR>hxy₂ : 0 ≤ ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>h : ‖x‖ ^ 2 + 2 * ⟪x, y⟫_ℝ + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2<VAR>hxy₁ : 0 ≤ ‖x + y‖<VAR>hxy₂ : 0 ≤ ‖x‖ + ‖y‖<GOAL>⟪x, y⟫_ℝ = ‖x‖ * ‖y‖
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<GOAL>log b r = 0
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<VAR>h : 1 ≤ r<GOAL>log b r = 0
<VAR>R : Type u_1<VAR>inst✝¹ : LinearOrderedSemifield R<VAR>inst✝ : FloorSemiring R<VAR>b : ℕ<VAR>hb : b ≤ 1<VAR>r : R<VAR>h : r ≤ 1<GOAL>log b r = 0
<VAR>a : ℕ<GOAL>jacobiSymNat a 1 = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<VAR>h : n ≤ m<GOAL>Even (m - n)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>hm : Odd m<VAR>hn : Odd n<VAR>h : m ≤ n<GOAL>Even (m - n)
<VAR>R : Type u_1<VAR>inst✝⁸ : Ring R<VAR>M : Type u_2<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M₂ : Type u_3<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : TopologicalAddGroup M<VAR>inst✝ : T1Space M<VAR>p : Submodule R M<VAR>f : M →L[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<GOAL>IsClosed ↑p
<VAR>R : Type u_1<VAR>inst✝⁸ : Ring R<VAR>M : Type u_2<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>M₂ : Type u_3<VAR>inst✝⁴ : TopologicalSpace M₂<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : TopologicalAddGroup M<VAR>inst✝ : T1Space M<VAR>p : Submodule R M<VAR>f : M →L[R] ↥p<VAR>hf : ∀ (x : ↥p), f ↑x = x<VAR>this : LinearMap.ker (ContinuousLinearMap.id R M - p.subtypeL.comp f) = p<GOAL>IsClosed ↑p
<VAR>𝕂 : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>n' : m → Type u_5<VAR>𝔸 : Type u_6<VAR>inst✝⁹ : RCLike 𝕂<VAR>inst✝⁸ : Fintype m<VAR>inst✝⁷ : DecidableEq m<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : (i : m) → Fintype (n' i)<VAR>inst✝³ : (i : m) → DecidableEq (n' i)<VAR>inst✝² : NormedCommRing 𝔸<VAR>inst✝¹ : NormedAlgebra 𝕂 𝔸<VAR>inst✝ : CompleteSpace 𝔸<VAR>U A : Matrix m m 𝔸<VAR>hy : IsUnit U<VAR>u : (Matrix m m 𝔸)ˣ<VAR>hu : ↑u = U<GOAL>exp 𝕂 (↑u * A * (↑u)⁻¹) = ↑u * exp 𝕂 A * (↑u)⁻¹
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl<GOAL>x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : ↑(ProjectiveSpectrum.top 𝒜)<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl<GOAL>↑f.den ∉ x.asHomogeneousIdeal
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : ConditionallyCompleteLattice α<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>f : ι → α<VAR>a : α<GOAL>s.sup' H f ≤ a ↔ sSup (f '' ↑s) ≤ a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x✝ y✝ x y : R<GOAL>(mk I) x = (mk I) y ↔ x - y ∈ I
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>f₀ f₁ : F → 𝕜<VAR>f₀' f₁' x₀ x₁ : F<VAR>s₀ s₁ t : Set F<VAR>L₀ L₁ : Filter F<VAR>h : HasGradientWithinAt f f' s x<VAR>hs : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f x<GOAL>s ⊆ s
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Surjective ⇑f'<VAR>n : ℕ<GOAL>Surjective ⇑(f' ^ (n + 1))
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Surjective ⇑f'<VAR>n : ℕ<GOAL>Surjective ⇑((f' ^ n) ∘ₗ f')
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : SemilatticeSup α<VAR>inst✝² : SemilatticeSup β<VAR>ι : Sort u_4<VAR>S : Set (Set α)<VAR>f✝ : ι → Set α<VAR>s t : Set α<VAR>a✝ : α<VAR>inst✝¹ : FunLike F β α<VAR>inst✝ : SupHomClass F β α<VAR>hs : SupClosed s<VAR>f : F<VAR>a : β<VAR>ha : a ∈ ⇑f ⁻¹' s<VAR>b : β<VAR>hb : b ∈ ⇑f ⁻¹' s<GOAL>a ⊔ b ∈ ⇑f ⁻¹' s
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>x : (i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i<VAR>f : R ⧸ ∏ i ∈ s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) := quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = x ⟨i, hi⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>f : R ⧸ ∏ i ∈ s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) := quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯<VAR>y : R ⧸ ∏ i ∈ s, P i ^ e i<GOAL>∃ y_1, ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y_1 = f y ⟨i, hi⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain R<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>P : ι → Ideal R<VAR>e : ι → ℕ<VAR>prime : ∀ i ∈ s, Prime (P i)<VAR>coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j<VAR>f : R ⧸ ∏ i ∈ s, P i ^ e i ≃+* ((i : { x // x ∈ s }) → R ⧸ P ↑i ^ e ↑i) := quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯<VAR>z : R<GOAL>∃ y, ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = f ((Ideal.Quotient.mk (∏ i ∈ s, P i ^ e i)) z) ⟨i, hi⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>‖∑' (n : ℕ), x ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>‖x ^ 0 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>‖1 + ∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this : ‖∑' (b : ℕ), (fun n => x ^ (n + 1)) b‖ ≤ (1 - ‖x‖)⁻¹ - 1<GOAL>‖1‖ + ‖∑' (b : ℕ), x ^ (b + 1)‖ ≤ ‖1‖ - 1 + (1 - ‖x‖)⁻¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>n : ℕ<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>v : Fin n → M<GOAL>(liftAlternating f) ((ιMulti R n) v) = (f n) v
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>N' : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : AddCommGroup N'<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module R N'<VAR>n : ℕ<VAR>f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N<VAR>v : Fin n → M<GOAL>(liftAlternating f) (List.ofFn fun i => (ι R) (v i)).prod = (f n) v
<VAR>a : ℤ<VAR>n : ℕ<GOAL>pred^[n + 1] a = a - ↑(n + 1)
<VAR>a : ℤ<VAR>n : ℕ<GOAL>(pred ∘ pred^[n]) a = a - ↑n - 1
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<VAR>this : Semigroup M' := Semigroup.mk ⋯<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<VAR>this✝ : Semigroup M' := Semigroup.mk ⋯<VAR>this : CompactSpace M'<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<VAR>this✝¹ : Semigroup M' := Semigroup.mk ⋯<VAR>this✝ : CompactSpace M'<VAR>this : Nonempty M'<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<VAR>this✝² : Semigroup M' := Semigroup.mk ⋯<VAR>this✝¹ : CompactSpace M'<VAR>this✝ : Nonempty M'<VAR>this : ∀ (p : M'), Continuous fun x => x * p<GOAL>∃ m ∈ s, m * m = m
<VAR>M : Type u_1<VAR>inst✝² : Semigroup M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : T2Space M<VAR>continuous_mul_left : ∀ (r : M), Continuous fun x => x * r<VAR>s : Set M<VAR>snemp : s.Nonempty<VAR>s_compact : IsCompact s<VAR>s_add : ∀ x ∈ s, ∀ y ∈ s, x * y ∈ s<VAR>M' : Type u_1 := { m // m ∈ s }<VAR>this✝² : Semigroup M' := Semigroup.mk ⋯<VAR>this✝¹ : CompactSpace M'<VAR>this✝ : Nonempty M'<VAR>this : ∀ (p : M'), Continuous fun x => x * p<VAR>m : M<VAR>hm : m ∈ s<VAR>idem : ⟨m, hm⟩ * ⟨m, hm⟩ = ⟨m, hm⟩<GOAL>∃ m ∈ s, m * m = m
<VAR>α : Type u_1<VAR>inst✝ : CommGroupWithZero α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>hmn : m.Coprime n<VAR>a : α<GOAL>(a ^ m ∈ Set.range fun x => x ^ n) ↔ a ∈ Set.range fun x => x ^ n
<VAR>α : Type u_1<VAR>inst✝ : CommGroupWithZero α<VAR>a✝ b : α<VAR>m n : ℕ<VAR>hmn : m.Coprime n<VAR>a : α<GOAL>(∃ y c, y = c ^ m ∧ a = c ^ n) ↔ ∃ y, y ^ n = a
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ * gaussSum χ ψ = gaussSum χ ψ * (gaussSum χ ψ⁻¹ * χ (-1))
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>gaussSum χ ψ = gaussSum χ ψ⁻¹ * χ (-1)
<VAR>R : Type u<VAR>inst✝³ : Field R<VAR>inst✝² : Fintype R<VAR>R' : Type v<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ₁ : χ ≠ 1<VAR>hχ₂ : χ.IsQuadratic<VAR>ψ : AddChar R R'<VAR>hψ : ψ.IsPrimitive<GOAL>χ ↑(-1) * gaussSum χ (ψ.mulShift ↑(-1)) = χ (-1) * gaussSum χ (ψ.mulShift (-1))
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<GOAL>Homotopic p q → Path.Homotopic (toLoop i p) (toLoop i q)
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t : ↑I × ↑I<GOAL>(homotopyTo i H) t ∈ Ω^ { j // j ≠ i } X x
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>Continuous fun t => ⟨(homotopyTo i H) t, ⋯⟩
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (x_1 : ↑I), { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ?refine_2 }.toFun (0, x_1) = (toLoop i p).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (x_1 : ↑I), { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ?refine_2 }.toFun (1, x_1) = (toLoop i q).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (t x_1 : ↑I), x_1 ∈ {0, 1} → { toFun := fun x_2 => { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ?refine_2, map_zero_left := ?refine_3, map_one_left := ?refine_4 }.toFun (t, x_2), continuous_toFun := ⋯ } x_1 = (toLoop i p).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (x_1 : ↑I), { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (0, x_1) = (toLoop i p).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (x_1 : ↑I), { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) = (toLoop i q).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (t x_1 : ↑I), x_1 ∈ {0, 1} → { toFun := fun x_2 => { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ?refine_3, map_one_left := ?refine_4 }.toFun (t, x_2), continuous_toFun := ⋯ } x_1 = (toLoop i p).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>x✝ : ↑I<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>x✝ : ↑I<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<GOAL>∀ (t x_1 : ↑I), x_1 ∈ {0, 1} → { toFun := fun x_2 => { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x_2), continuous_toFun := ⋯ } x_1 = (toLoop i p).toContinuousMap x_1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t y : ↑I<VAR>yH : y ∈ {0, 1}<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>({ toFun := fun x_1 => { toFun := fun t => ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x_1), continuous_toFun := ⋯ } y) y✝ = ((toLoop i p).toContinuousMap y) y✝
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t y : ↑I<VAR>yH : y ∈ {0, 1}<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>H ((t, y).1, (Cube.insertAt i) ((t, y).2, y✝)) = ((toLoop i p).toContinuousMap y) y✝
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t y : ↑I<VAR>yH : y ∈ {0, 1}<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>(Cube.insertAt i) ((t, y).2, y✝) ∈ Cube.boundary N
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t y : ↑I<VAR>yH : y ∈ {0, 1}<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>(Cube.insertAt i) ((t, y).2, y✝) i = 0 ∨ (Cube.insertAt i) ((t, y).2, y✝) i = 1
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p q : ↑(Ω^ N X x)<VAR>H : (↑p).HomotopyRel (↑q) (Cube.boundary N)<VAR>t y : ↑I<VAR>yH : y ∈ {0, 1}<VAR>y✝ : { j // j ≠ i } → ↑I<GOAL>((t, y).2, y✝).1 = 0 ∨ ((t, y).2, y✝).1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderClosedTopology β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f g : α → β<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>this✝¹ : MeasurableSpace (β × β) := borel (β × β)<VAR>this✝ : BorelSpace (β × β)<GOAL>MeasurableSet {a | f a < g a}
<VAR>a b c : EReal<GOAL>a * (b * c⁻¹) = a * b * c⁻¹
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<GOAL>SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>z : N<VAR>H : f ↑y * z = 1<GOAL>↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : M →* N<VAR>h : ∀ (y : ↥S), IsUnit (f ↑y)<VAR>y : ↥S<VAR>z : N<VAR>H : f ↑y * z = 1<GOAL>↑1 = f ↑y * z
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>γ : Type u_2<VAR>s : TopologicalSpace β<VAR>B₁ : Set (Set α)<VAR>B₂ : Set (Set β)<VAR>h₁ : IsTopologicalBasis B₁<VAR>h₂ : IsTopologicalBasis B₂<VAR>f₁ : γ → α<VAR>f₂ : γ → β<GOAL>IsTopologicalBasis (image2 (fun x x_1 => f₁ ⁻¹' x ∩ f₂ ⁻¹' x_1) B₁ B₂)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<VAR>X : C<GOAL>e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫ (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X) = 𝟙 (e.functor.unop.obj X)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>e : Cᵒᵖ ≌ Dᵒᵖ<VAR>X : C<GOAL>(e.functor.unop.map ((NatIso.unop e.unitIso).symm.hom.app X) ≫ (NatIso.unop e.counitIso).symm.hom.app (e.functor.unop.obj X)).op = (𝟙 (e.functor.unop.obj X)).op
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n.succ = succ ↑n
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n + 1 = succ ↑n
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n < ↑n + 1
<VAR>α β : Type u<VAR>n : ℕ<GOAL>↑n < ↑n.succ
<VAR>n : ℕ∞<GOAL>1 ≤ ↑n ↔ 1 ≤ n
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute b a<GOAL>⅟b * a = ⅟b * (a * b * ⅟b)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute b a<GOAL>⅟b * (a * b * ⅟b) = ⅟b * (b * a * ⅟b)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<VAR>h : Commute b a<GOAL>⅟b * (b * a * ⅟b) = a * ⅟b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : StrictMono f<VAR>hg : Monotone g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x ≤ g^[n] x ↔ f x ≤ g x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>comap (fun x => (inclusion hst x.1, inclusion hst x.2)) (𝓤 ↑t) = 𝓤 ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s t : Set α<VAR>hst : s ⊆ t<GOAL>comap ((fun q => (↑q.1, ↑q.2)) ∘ fun x => (inclusion hst x.1, inclusion hst x.2)) (𝓤 α) = comap (fun q => (↑q.1, ↑q.2)) (𝓤 α)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : BooleanAlgebra α<VAR>s✝ s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b c : α<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>n : ℕ<VAR>h𝒜 : Set.Sized n ↑𝒜<VAR>s : Finset α<VAR>hs : s ∈ 𝒜<GOAL>sᶜ.card = Fintype.card α - n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>f : α → β<GOAL>(bind 0 fun x => {f x}) = map f 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>a : α<VAR>s t : Multiset α<VAR>f✝ g : α → Multiset β<VAR>f : α → β<GOAL>∀ (a : α) (s : Multiset α), (s.bind fun x => {f x}) = map f s → ((a ::ₘ s).bind fun x => {f x}) = map f (a ::ₘ s)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>J : GrothendieckTopology C<VAR>P : Cᵒᵖ ⥤ A<VAR>X✝ : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>E : Aᵒᵖ<VAR>π : (S.arrows.diagram.op ⋙ P).cones.obj E<VAR>X Y : C<VAR>f : X ⟶ X✝<VAR>g : Y ⟶ X<VAR>hf : S.arrows f<GOAL>(fun Y f h => π.app (op { obj := Over.mk f, property := h })) Y (g ≫ f) ⋯ = (P ⋙ coyoneda.obj E).map g.op ((fun Y f h => π.app (op { obj := Over.mk f, property := h })) X f hf)