ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) = cexp (-↑π * I * (τ + 2 * z) + (2 * ↑π * I * (↑n + ↑1) * z + ↑π * I * (↑n + ↑1) ^ 2 * τ))
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>σ τ : p.Gal<VAR>h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x<GOAL>σ = τ
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>p q : F[X]<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>σ τ : p.Gal<VAR>h : ∀ x ∈ p.rootSet p.SplittingField, σ x = τ x<VAR>x : p.SplittingField<GOAL>AlgHom.equalizer ↑σ ↑τ = ⊤
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal ≤ rexp (-t * ε) * mgf X μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal ≤ rexp (- -t * -ε) * mgf (-X) μ (-t)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>(μ {ω | X ω ≤ ε}).toReal = (μ {ω | -ε ≤ (-X) ω}).toReal
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>ε : ℝ<VAR>ht : t ≤ 0<VAR>h_int : Integrable (fun ω => rexp (t * X ω)) μ<GOAL>Integrable (fun ω => rexp (-t * (-X) ω)) μ
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>s t : Set α✝<VAR>α : Type u_3<GOAL>∅.ncard = 0
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • ∑ i : Fin 2, f (![![a, b], ![b, a]] i)<GOAL>False
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]<GOAL>False
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]<VAR>sharp : 2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < 2 • (Multiset.map (fun r => f r) (ω.tt ![![a, b], ![b, a]])).sum<GOAL>False
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]<VAR>sharp : 2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < 2 • (Multiset.map (fun r => f r) (ω.tt ![![a, b], ![b, a]])).sum<VAR>impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]<GOAL>False
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]<VAR>sharp : 2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < 2 • (Multiset.map (fun r => f r) (ω.tt ![![a, b], ![b, a]])).sum<VAR>impos : 2 • (Multiset.map (fun x => f ![a, b]) ω).sum < ω.size • 2 • f ![a, b]<VAR>rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]<GOAL>False
<VAR>D : Type u_1<VAR>C✝ : Type u_2<VAR>inst✝¹ : OrderedAddCommMonoid C✝<VAR>m : ℕ<VAR>C : Type u_3<VAR>inst✝ : OrderedCancelAddCommMonoid C<VAR>f : (Fin 2 → D) → C<VAR>ω : FractionalOperation D 2<VAR>valid : ω.IsValid<VAR>symmega : ω.IsSymmetric<VAR>a b : D<VAR>hab : a ≠ b<VAR>mcfab : HasMaxCutPropertyAt f a b<VAR>contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]<VAR>sharp : 2 • (Multiset.map (fun x => f ![a, b]) (ω.tt ![![a, b], ![b, a]])).sum < 2 • (Multiset.map (fun r => f r) (ω.tt ![![a, b], ![b, a]])).sum<VAR>impos : 2 • ω.size • f ![a, b] < 2 • ω.size • f ![a, b]<VAR>rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b]<VAR>distrib : (Multiset.map (fun x => f ![a, b]) ω).sum = ω.size • f ![a, b]<GOAL>False
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<GOAL>0 < eval (-1) (cyclotomic n R)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<GOAL>0 < eval (-1) (cyclotomic n R)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<GOAL>0 < eval (↑(-1)) (cyclotomic n ℤ)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<GOAL>0 < eval (↑(-1)) (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<GOAL>0 < eval (-1) (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<VAR>h0 : (cyclotomic n ℝ).coeff 0 = 1<GOAL>0 < eval (-1) (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<GOAL>0 < eval (-1) (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<VAR>hx : eval (-1) (cyclotomic n ℝ) ≤ 0<GOAL>False
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this✝ : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<VAR>hx : eval (-1) (cyclotomic n ℝ) ≤ 0<VAR>this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)<GOAL>False
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this✝ : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<VAR>hx : eval (-1) (cyclotomic n ℝ) ≤ 0<VAR>this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)<VAR>y : ℝ<VAR>hy : (cyclotomic n ℝ).IsRoot y<GOAL>False
<VAR>n : ℕ<VAR>hn : 2 < n<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this✝ : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<VAR>hx : eval (-1) (cyclotomic n ℝ) ≤ 0<VAR>this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)<VAR>y : ℝ<VAR>hy : IsPrimitiveRoot y n<GOAL>False
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>this✝ : NeZero n<VAR>h0 : eval 0 (cyclotomic n ℝ) = 1<VAR>hx : eval (-1) (cyclotomic n ℝ) ≤ 0<VAR>this : Set.Icc (eval (-1) (cyclotomic n ℝ)) (eval 0 (cyclotomic n ℝ)) ⊆ Set.range fun x => eval x (cyclotomic n ℝ)<VAR>y : ℝ<VAR>hn : 2 < orderOf y<VAR>hy : IsPrimitiveRoot y n<GOAL>False
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).ψ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).ψ n)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hIY : I ⊆ Y<VAR>hYX : Y ⊆ X<GOAL>M.Basis I Y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>hIY : I ⊆ Y<VAR>hYX : Y ⊆ X<GOAL>∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
<VAR>θ : Angle<GOAL>(2 • θ).toReal = 2 * θ.toReal - 2 * π ↔ π / 2 < θ.toReal
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<VAR>p p' : Perm α'<VAR>x✝ : β'<GOAL>(Equiv.trans (e.permCongr p) (e.permCongr p')) x✝ = (e.permCongr (Equiv.trans p p')) x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s : Set X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<VAR>b : Y<GOAL>(𝓝 b).HasBasis (?m.187297 b) (?m.187298 b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s : Set X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<VAR>b : Y<GOAL>(comap f (𝓝 (f b))).HasBasis (?m.187297 b) (?m.187298 b)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : RegularSpace X<VAR>x : X<VAR>s✝ : Set X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Y → X<VAR>hf : Inducing f<VAR>b : Y<VAR>s : Set X<VAR>hs : s ∈ 𝓝 (f b) ∧ IsClosed s<GOAL>IsClosed (f ⁻¹' id s)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>(∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2
<VAR>x : ℝ≥0<GOAL>↑(⊤ * ↑x) = ⊤ * ↑↑x
<GOAL>↑(⊤ * ↑0) = ⊤ * ↑↑0
<VAR>x : ℝ≥0<VAR>h0 : x ≠ 0<GOAL>↑(⊤ * ↑x) = ⊤ * ↑↑x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hq : 0 ≤ q<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊<GOAL>∫⁻ (a : α), ↑‖f a‖₊ ^ q ∂μ ≤ ∫⁻ (a : α), ↑‖g a‖₊ ^ q ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>g : α → G<VAR>hq : 0 ≤ q<VAR>h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊<VAR>x : α<VAR>hx : ‖f x‖₊ ≤ ‖g x‖₊<GOAL>↑‖f x‖₊ ^ q ≤ ↑‖g x‖₊ ^ q
<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>r : R<VAR>b : CliffordAlgebra Q<GOAL>(contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d = (algebraMap R (CliffordAlgebra Q)) r * (contractRight b) d
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>s : Set K<VAR>hs : IsTranscendenceBasis ℤ Subtype.val<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>s : Set K<VAR>hs : IsTranscendenceBasis ℤ Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis ℤ Subtype.val<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>s : Set K<VAR>hs : IsTranscendenceBasis ℤ Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis ℤ Subtype.val<VAR>this : #↑s = #↑t<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : IsAlgClosed K<VAR>inst✝² : IsAlgClosed L<VAR>inst✝¹ : CharZero K<VAR>inst✝ : CharZero L<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>s : Set K<VAR>hs : IsTranscendenceBasis ℤ Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis ℤ Subtype.val<VAR>this : #↑s = #↑t<VAR>e : ↑s ≃ ↑t<GOAL>Nonempty (K ≃+* L)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝⁴ : MonoidWithZero R<VAR>inst✝³ : MonoidWithZero S<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : SMulCommClass R S S<VAR>inst✝ : IsScalarTower R S S<VAR>a : S<VAR>t : R<VAR>k : ℕ<VAR>ha : a ^ k = 0<GOAL>IsNilpotent (t • a)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝⁴ : MonoidWithZero R<VAR>inst✝³ : MonoidWithZero S<VAR>inst✝² : MulActionWithZero R S<VAR>inst✝¹ : SMulCommClass R S S<VAR>inst✝ : IsScalarTower R S S<VAR>a : S<VAR>t : R<VAR>k : ℕ<VAR>ha : a ^ k = 0<GOAL>(t • a) ^ k = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : TopologicalSpace M₂<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : TopologicalAddGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R M₂<VAR>x✝¹ : M →L[R] M<VAR>x✝ : M<GOAL>(Ring.inverse x✝¹) x✝ = x✝¹.inverse x✝
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X✝ Y : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>B : C<VAR>I : Type u_1<VAR>X : I → C<VAR>π : (i : I) → X i ⟶ B<VAR>inst✝ : (ofArrows X π).hasPullbacks<GOAL>IsSheafFor P (ofArrows X π) ↔ ∀ (x : (i : I) → P.obj (op (X i))), Arrows.PullbackCompatible P π x → ∃! t, ∀ (i : I), P.map (π i).op t = x i
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<GOAL>(fun x => x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<GOAL>x ∈ closure s ↔ (comap Subtype.val (𝓝 x)).NeBot
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : (i : α) → Set (β i)<VAR>f : (i : { x // p x }) → β ↑i<VAR>g : (i : { x // ¬p x }) → β ↑i<GOAL>(f, g) ∈ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s ↔ (f, g) ∈ (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : (i : α) → Set (β i)<VAR>f : (i : { x // p x }) → β ↑i<VAR>g : (i : { x // ¬p x }) → β ↑i<GOAL>(∀ (i : α), (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i) ↔ ∀ (x : α), (∀ (b : p x), f ⟨x, b⟩ ∈ s x) ∧ ∀ (b : ¬p x), g ⟨x, b⟩ ∈ s x
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>s : (i : α) → Set (β i)<VAR>f : (i : { x // p x }) → β ↑i<VAR>g : (i : { x // ¬p x }) → β ↑i<VAR>i : α<GOAL>(piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : 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>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (image₂ f s t).Nonempty<GOAL>(image₂ f s t).sup' h g = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : 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>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : SemilatticeSup δ<VAR>g : γ → δ<VAR>h : (image₂ f s t).Nonempty<GOAL>(t.sup' ⋯ fun i' => s.sup' ⋯ fun i => (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y => s.sup' ⋯ fun x => g (f x y)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : Finite ι<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : Module 𝕜 F<GOAL>Continuous fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : Finite ι<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : Module 𝕜 F<VAR>val✝ : Fintype ι<GOAL>Continuous fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : Finite ι<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : Module 𝕜 F<VAR>val✝ : Fintype ι<VAR>x✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<GOAL>Continuous fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : Finite ι<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : Module 𝕜 F<VAR>val✝ : Fintype ι<VAR>x✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<GOAL>Continuous fun p => p.1 p.2
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : Finite ι<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : Module 𝕜 F<VAR>val✝ : Fintype ι<VAR>x✝ : UniformSpace F := TopologicalAddGroup.toUniformSpace F<VAR>this : UniformAddGroup F<VAR>m : (i : ι) → E i<GOAL>∃ V ∈ {s | Bornology.IsVonNBounded 𝕜 s}, V ∈ 𝓝 m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<GOAL>univ.Pairwise r ↔ Pairwise r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>b : Ordinal.{u_4}<VAR>h₁ : 0 ∣ b<VAR>h₂ : b ∣ 0<GOAL>0 = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>a0 : ¬a = 0<VAR>h₁ : a ∣ 0<VAR>h₂ : 0 ∣ a<GOAL>a = 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : 0 < b<VAR>x✝ : c + b * d = a ∧ c < b<VAR>h₁ : c + b * d = a<VAR>h₂ : c < b<GOAL>(c + b * d) / b = d ∧ (c + b * d) % b = c
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : 0 < b<VAR>x✝ : c + b * d = a ∧ c < b<VAR>h₁ : c + b * d = a<VAR>h₂ : c < b<GOAL>c / b + d = d ∧ c % b = c
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>inst✝² : Fintype M<VAR>inst✝¹ : DecidableEq M<VAR>R : Type u_2<VAR>inst✝ : CommMonoidWithZero R<VAR>ζ : Rˣ<VAR>hζ : ζ ∈ rootsOfUnity (Monoid.orderUnits M) R<VAR>g : Mˣ<VAR>hg : ∀ (x : Mˣ), x ∈ Subgroup.zpowers g<GOAL>(ofRootOfUnity hζ hg) ↑g = ↑ζ
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n : ℕ<VAR>z : ℤ<VAR>x✝ : a₁ ≡ b₁ [PMOD p]<VAR>m : ℤ<VAR>hm : b₁ - a₁ = m • p<GOAL>(∃ b, b₁ + b₂ - (a₁ + a₂) = (Equiv.symm (Equiv.addLeft m)).symm b • p) ↔ a₂ ≡ b₂ [PMOD p]
<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>x : M ⊗[R] N<GOAL>(lTensor M (g ∘ₗ f)) x = (lTensor M g) ((lTensor M f) x)
<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>x : M ⊗[R] N<GOAL>(⇑(lTensor M g) ∘ ⇑(lTensor M f)) x = (lTensor M g) ((lTensor M f) x)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f g : R[X]<VAR>N n✝ : ℕ<GOAL>(reflect N (f + g)).coeff n✝ = (reflect N f + reflect N g).coeff n✝
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>F : Type u_4<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : AlgHomClass F R A B<VAR>φ ψ : F<GOAL>equalizer φ ψ = ⊤ ↔ φ = ψ
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝ : IsWellOrder α r<VAR>o₁ o₂ : Ordinal.{u}<VAR>h₁ : o₁ < type r<VAR>h₂ : o₂ < type r<GOAL>r (enum r o₁ h₁) (enum r o₂ h₂) ↔ o₁ < o₂
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : FiniteDimensional F E<VAR>inst✝ : IsGalois F E<VAR>α : E<VAR>hα : F⟮α⟯ = ⊤<VAR>iso : ↥F⟮α⟯ ≃ₐ[F] E := { toFun := fun e => ↑e, invFun := fun e => ⟨e, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }<VAR>H : IsIntegral F α<GOAL>Fintype.card (E ≃ₐ[F] E) = finrank F E