ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ✝ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>μ : Measure (E × ℝ)<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>ν : Measure E := addHaar<VAR>A : ν.prod volume = (ν.prod volume).addHaarScalarFactor μ • μ<VAR>Hf'g : Integrable (fun x => (B (f' x)) (g x)) (ν.prod volume)<VAR>Hfg' : Integrable (fun x => (B (f x)) (g' x)) (ν.prod volume)<VAR>Hfg : Integrable (fun x => (B (f x)) (g x)) (ν.prod volume)<GOAL>∫ (x : E × ℝ), (B (f x)) (g' x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.addHaarScalarFactor (ν.prod volume) • ν.prod volume
<VAR>x y : ℤ<GOAL>(toComplex { re := x, im := y }).re = ↑x
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<GOAL>((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)<GOAL>((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr ()) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)<GOAL>((listTransvecCol (M * (listTransvecRow M).prod)).prod * (M * (listTransvecRow M).prod)) (inl i) (inr ()) = 0
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq p<VAR>inst✝ : CommRing R<VAR>r : ℕ<VAR>M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>hM : M (inr ()) (inr ()) ≠ 0<VAR>i : Fin r<VAR>this : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod)<GOAL>(M * (listTransvecRow M).prod) (inr ()) (inr ()) ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(↑n).natDegree = 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>s' : Fin n → R<VAR>f : (MvPolynomial (Fin n) R)[X]<VAR>i : ℕ<GOAL>(Polynomial.map (eval s') f).coeff i = (eval s') (f.coeff i)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : M' → M''<VAR>hg : ContMDiff I' I'' n g<VAR>hf : ContMDiff I I' n f<GOAL>ContMDiff I I'' n (g ∘ f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁶ : NormedAddCommGroup E<VAR>inst✝¹⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace H M<VAR>inst✝¹¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁷ : TopologicalSpace M'<VAR>inst✝⁶ : ChartedSpace H' M'<VAR>inst✝⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : M' → M''<VAR>hg : ContMDiffOn I' I'' n g univ<VAR>hf : ContMDiffOn I I' n f univ<GOAL>ContMDiffOn I I'' n (g ∘ f) univ
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<VAR>x₀ : X<GOAL>EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt Subtype.val S x₀
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n : ℕ<VAR>a : R<VAR>i : ℕ<VAR>h : i ≠ n<GOAL>(p.update n a).coeff i = p.coeff i
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>(filter p s).prod * (filter (fun a => ¬p a) s).prod = s.prod
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>h : ∀ (i : n), A i j = 0<GOAL>A.det = 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>h : ∀ (i : n), A i j = 0<GOAL>Aᵀ.det = 0
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i j : Fin n<VAR>a : Fin (n + 2)<VAR>b : Fin (n + 1)<VAR>ha : a ≠ last (n + 1)<VAR>hb : b ≠ last n<VAR>hk : optParam (a.succAbove b ≠ last (n + 1)) ⋯<GOAL>(a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
<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 : α → M<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hf : (mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset.erase a, f i
<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 : α → M<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hf : (mulSupport f).Finite<GOAL>∀ {x : α}, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset.erase a)
<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 : α → M<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hf : (mulSupport f).Finite<VAR>x : α<VAR>hx : f x ≠ 1<GOAL>x ≠ a ↔ x ∈ hf.toFinset.erase a
<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 : α → M<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>hf : (mulSupport f).Finite<VAR>x : α<VAR>hx : f x ≠ 1<GOAL>x ≠ a ↔ x ≠ a ∧ f x ≠ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>hab : a < b<GOAL>Ioo a b ∪ {b} = Ioc a b
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>h : hζ.toInteger - ↑n = ↑↑p * x<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>h : hζ.toInteger - ↑n = ↑↑p * x<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : pB.dim = ↑p ^ k * (↑p - 1)<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>h : hζ.toInteger - ↑n = ↑↑p * x<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>h : hζ.toInteger = ↑↑p * x + ↑n<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩<VAR>this : pB.basis ⟨1, hdim⟩ = pB.gen ^ ↑⟨1, hdim⟩<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩<VAR>this : pB.basis ⟨1, hdim⟩ = hζ.toInteger ^ ↑⟨1, hdim⟩<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>h : (pB.basis.repr hζ.toInteger) ⟨1, hdim⟩ = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩<VAR>this : pB.gen = hζ.toInteger<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>h : (if ⟨1, hdim⟩ = ⟨1, hdim⟩ then 1 else 0) = (pB.basis.repr (↑↑p * x + ↑n)) ⟨1, hdim⟩<VAR>this : pB.gen = hζ.toInteger<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>this : pB.gen = hζ.toInteger<VAR>h : 1 = (pB.basis.repr (↑↑p * x)) ⟨1, hdim⟩ + (pB.basis.repr ↑n) ⟨1, hdim⟩<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>this : pB.gen = hζ.toInteger<VAR>h : 1 = ↑↑p • (pB.basis.repr x) ⟨1, hdim⟩ + n • if ⟨0, ⋯⟩ = ⟨1, hdim⟩ then 1 else 0<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>htwo : p ^ (k + 1) ≠ 2<VAR>n : ℤ<VAR>x : 𝓞 K<VAR>pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasis<VAR>hdim : 1 < pB.dim<VAR>this : pB.gen = hζ.toInteger<VAR>h : 1 = ↑↑p * (pB.basis.repr x) ⟨1, hdim⟩<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Group α<VAR>a✝ : α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ᵐ / a⁺ᵐ = a⁻¹
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ : DirichletCharacter R n<VAR>m : ℕ<VAR>hm : n ∣ m<VAR>a : (ZMod m)ˣ<GOAL>((changeLevel hm) χ) ↑a = χ (↑a).cast
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : OrderedCommGroup α<VAR>inst✝ : OrderedCommGroup β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<GOAL>MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝⁵ : TopologicalSpace B'<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>f : B' → B<VAR>x : B'<GOAL>Continuous (TotalSpace.mk x)
<VAR>B : Type u<VAR>F : Type v<VAR>E : B → Type w₁<VAR>B' : Type w₂<VAR>f✝ : B' → B<VAR>inst✝⁵ : TopologicalSpace B'<VAR>inst✝⁴ : TopologicalSpace (TotalSpace F E)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>f : B' → B<VAR>x : B'<GOAL>instTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { proj := x, snd := x_1 }) inst✝⁴
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → α<VAR>h : EqOn f id s<GOAL>f '' s = s
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>x t.take.take * y t.take.drop * z t.drop = cast ⋯ (fun t => x t.take * (y t.drop.take * z t.drop.drop)) t
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) = (fun t => x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t
<VAR>α : Type<VAR>d : ℕ<VAR>ds ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Semigroup α<VAR>x : Holor α ds₁<VAR>y : Holor α ds₂<VAR>z : Holor α ds₃<VAR>t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)<GOAL>ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<GOAL>Nat.casesAuxOn (motive := fun a => 0 = a → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0 (fun h => if hp : -rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ = rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ then AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1 else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1) (fun n h => Eq.rec (motive := fun x x_1 => [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → E [⋀^Fin x]→ₗ[ℝ] ℝ) (fun [Fact (finrank ℝ E = n + 1)] o => (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det) ⋯ (-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯)) ⋯ = -AlternatingMap.constLinearEquivOfIsEmpty 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<GOAL>¬-rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ = rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<GOAL>¬rayOfNeZero ℝ (-AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯ = rayOfNeZero ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) ⋯
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<GOAL>¬SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>_i✝ : Fact (finrank ℝ E = n)<VAR>o : Orientation ℝ E (Fin n)<VAR>_i : Fact (finrank ℝ E = 0)<VAR>h : SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)<GOAL>False
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r✝ r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>r : ℝ≥0∞<GOAL>a ∈ EMetric.ball 1 r ↔ ↑‖a‖₊ < r
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝² : NonUnitalNormedRing E<VAR>inst✝¹ : StarRing E<VAR>inst✝ : CstarRing E<VAR>x : E<GOAL>x * x⋆ = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P ≃ₗ[R] Q<VAR>f✝ : N ≃ₗ[R] P<VAR>m : M<VAR>n✝ : N<VAR>p : P<VAR>x : M ⊗[R] N<VAR>y : N ⊗[R] M<VAR>f : N ≃ₗ[R] N<VAR>n : ℤ<GOAL>lTensor M f ^ n = lTensor M (f ^ n)
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x r y : ℝ<GOAL>y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f✝ g : ι → M<VAR>s t : Finset ι<VAR>f : ι → M<VAR>h₁ : ∏ i ∈ s, f i = 1<VAR>h₂ : ∃ i ∈ s, f i ≠ 1<GOAL>∃ i ∈ s, 1 < f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f✝ g : ι → M<VAR>s t : Finset ι<VAR>f : ι → M<VAR>h₂ : ∃ i ∈ s, f i ≠ 1<VAR>h₁ : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, f i ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f✝ g : ι → M<VAR>s t : Finset ι<VAR>f : ι → M<VAR>h₁ : ∀ i ∈ s, f i ≤ 1<VAR>i : ι<VAR>m : i ∈ s<VAR>i_ne : f i ≠ 1<GOAL>∏ i ∈ s, f i ≠ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f✝ g : ι → M<VAR>s t : Finset ι<VAR>f : ι → M<VAR>h₁ : ∀ i ∈ s, f i ≤ 1<VAR>i : ι<VAR>m : i ∈ s<VAR>i_ne : f i ≠ 1<GOAL>∏ i ∈ s, f i < 1
<VAR>u v m n : ℤ<GOAL>Even (m + n) ↔ (Even m ↔ Even n)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>I : Type u<VAR>f : I → Type v<VAR>x✝ y : (i : I) → f i<VAR>i✝ j : I<VAR>α : Type u_3<VAR>β : α → Type u_4<VAR>γ : (a : α) → β a → Type u_5<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (β a)<VAR>inst✝ : (a : α) → (b : β a) → One (γ a b)<VAR>i : (a : α) × β a<VAR>x : γ i.fst i.snd<GOAL>curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>eval r p = p.smeval r
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>(p.sum fun e a => a * r ^ e) = p.sum (smul_pow r)
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<VAR>h : Nonempty M<VAR>this : Fintype M<GOAL>commProb M = 1 ↔ Commutative fun x x_1 => x * x_1
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<VAR>h : Nonempty M<VAR>this : Fintype M<GOAL>↑(card ↑{x | Commute x.1 x.2}) / ↑(card M) ^ 2 = 1 ↔ Commutative fun x x_1 => x * x_1
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<VAR>h : Nonempty M<VAR>this : Fintype M<GOAL>(∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ Commutative fun x x_1 => x * x_1
<VAR>M : Type u_1<VAR>inst✝¹ : Mul M<VAR>inst✝ : Finite M<VAR>h : Nonempty M<VAR>this : Fintype M<GOAL>↑(card M) ^ 2 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := {a} } ≤ { ofColex := s } ↔ ∃ x ∈ s, a ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>(a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s : ℝ<GOAL>(fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[cocompact ℝ] fun x => |x| ^ s
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℂ<VAR>ha : a.re < 0<VAR>b : ℂ<VAR>s : ℝ<GOAL>((fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atBot] fun x => |x| ^ s) ∧ (fun x => cexp (a * ↑x ^ 2 + b * ↑x)) =o[atTop] fun x => |x| ^ s
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<VAR>h : n < k<GOAL>multichoose (-↑n) k = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<VAR>h : n < k<GOAL>(fun x => k.factorial • x) (multichoose (-↑n) k) = (fun x => k.factorial • x) 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<VAR>h : n < k<GOAL>k.factorial • multichoose (-↑n) k = k.factorial • 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a✝ b c a : α<VAR>h : n ≠ 0<GOAL>|a ^ n| = 1 ↔ |a| = 1