ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<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>x y : L<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0<GOAL>y ∈ engel R x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<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>x y : L<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0<GOAL>∃ n, ((ad R L) x ^ n) y = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<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>x y : L<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0<GOAL>((ad R L) x ^ (n + 1)) y = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<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>x y : L<VAR>n : ℕ<VAR>hn : ((ad R L) x ^ n) ⁅x, y⁆ = 0<GOAL>((ad R L) x ^ n) (((ad R L) x) y) = 0
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulRightInvariant<VAR>inst✝ : ν.IsMulRightInvariant<GOAL>MeasurePreserving (fun z => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulRightInvariant<VAR>inst✝ : ν.IsMulRightInvariant<GOAL>(fun z => (z.1 * z.2, z.1⁻¹)) = (fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulRightInvariant<VAR>inst✝ : ν.IsMulRightInvariant<VAR>x y : G<GOAL>((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)) (x, y)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>(q - 1) ^ φ n < eval q (cyclotomic n ℝ)
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < Units.mk0 ‖eval (↑q) (cyclotomic n ℂ)‖₊ ⋯
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>Units.mk0 (q - 1).toNNReal ⋯ ^ φ n < ∏ i ∈ (primitiveRoots n ℂ).attach, Units.mk0 ‖↑q - ↑i‖₊ ⋯
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>Units.mk0 (q - 1).toNNReal ⋯ ^ φ n = ∏ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>{ x // x ∈ primitiveRoots n ℂ } → NNRealˣ
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>∀ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i ≤ Units.mk0 ‖↑q - ↑i‖₊ ⋯
<VAR>n : ℕ<VAR>q : ℝ<VAR>hn' : 2 ≤ n<VAR>hq' : 1 < q<VAR>hn : 0 < n<VAR>hq : 0 < q<VAR>hfor : ∀ ζ' ∈ primitiveRoots n ℂ, q - 1 ≤ ‖↑q - ζ'‖<VAR>ζ : ℂ := Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hex : ∃ ζ' ∈ primitiveRoots n ℂ, q - 1 < ‖↑q - ζ'‖<VAR>this : ¬eval (↑q) (cyclotomic n ℂ) = 0<GOAL>∃ i ∈ (primitiveRoots n ℂ).attach, ?convert_2 i < Units.mk0 ‖↑q - ↑i‖₊ ⋯
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>s : Set A<GOAL>s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ s
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>s : Set A<GOAL>(∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, id i ⊆ s) ↔ ∃ i, True ∧ ↑(B i) ⊆ s
<VAR>I : Type u<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : I → Type v₁<VAR>g : I → Type v₂<VAR>h : I → Type v₃<VAR>x y : (i : I) → f✝ i<VAR>i : I<VAR>inst✝ : Mul γ<VAR>f : α → β<VAR>g₁ g₂ : α → γ<VAR>e₁ e₂ : β → γ<GOAL>extend f (g₁ * g₂) (e₁ * e₂) = extend f g₁ e₁ * extend f g₂ e₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : Integrable f μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>Integrable (fun x => g x • f x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>Memℒp (fun x => g x • f x) 1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<GOAL>eLpNorm (fun x => g x • f x) 1 μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<VAR>h : 1 / 1 = 1 / ⊤ + 1 / 1<GOAL>eLpNorm (fun x => g x • f x) 1 μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : MeasurableSpace δ<VAR>inst✝³ : NormedAddCommGroup β<VAR>inst✝² : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 β<VAR>f : α → β<VAR>hf : Memℒp f 1 μ<VAR>g : α → 𝕜<VAR>g_aestronglyMeasurable : AEStronglyMeasurable g μ<VAR>ess_sup_g : essSup (fun x => ↑‖g x‖₊) μ ≠ ⊤<VAR>h : 1 / 1 = 1 / ⊤ + 1 / 1<VAR>hg' : eLpNorm g ⊤ μ ≠ ⊤<GOAL>eLpNorm (fun x => g x • f x) 1 μ < ⊤
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>inst✝ : IsDomain ↑R<GOAL>genericPoint ↑↑(Spec R).toPresheafedSpace = ⊥
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>inst✝ : IsDomain ↑R<GOAL>IsGenericPoint ⊥ ⊤
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>inst✝ : IsDomain ↑R<GOAL>closure {⊥} = ⊤
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>inst✝ : IsDomain ↑R<GOAL>PrimeSpectrum.zeroLocus ↑⊥.asIdeal = ⊤
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>inst✝ : IsDomain ↑R<GOAL>PrimeSpectrum.zeroLocus ↑⊥.asIdeal = PrimeSpectrum.zeroLocus {0}
<VAR>R : Type u_1<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : CharP R 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝² : NonAssocSemiring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : CharP R 1<VAR>this : Subsingleton R<GOAL>False
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>i j : ι<VAR>w : c.Rel i j<GOAL>f.next i = (C₁.xNextIso w).hom ≫ f.f j ≫ (C₂.xNextIso w).inv
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C C₁ C₂ C₃ : HomologicalComplex V c<VAR>f : C₁.Hom C₂<VAR>i : ι<VAR>w : c.Rel i (c.next i)<GOAL>f.next i = (C₁.xNextIso w).hom ≫ f.f (c.next i) ≫ (C₂.xNextIso w).inv
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.256266, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 3<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<GOAL>g.map' 0 1 ⋯ ⋯ ≫ app₁.inv = app₀.inv ≫ f.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.256266, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 3<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<GOAL>g.map' 1 2 ⋯ ⋯ ≫ app₂.inv = app₁.inv ≫ f.map' 1 2 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.256266, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>f g : ComposableArrows C 3<VAR>app₀ : f.obj' 0 ⋯ ≅ g.obj' 0 ⋯<VAR>app₁ : f.obj' 1 ⋯ ≅ g.obj' 1 ⋯<VAR>app₂ : f.obj' 2 ⋯ ≅ g.obj' 2 ⋯<VAR>app₃ : f.obj' 3 ⋯ ≅ g.obj' 3 ⋯<VAR>w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁.hom = app₀.hom ≫ g.map' 0 1 ⋯ ⋯<VAR>w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂.hom = app₁.hom ≫ g.map' 1 2 ⋯ ⋯<VAR>w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃.hom = app₂.hom ≫ g.map' 2 3 ⋯ ⋯<GOAL>g.map' 2 3 ⋯ ⋯ ≫ app₃.inv = app₂.inv ≫ f.map' 2 3 ⋯ ⋯
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c d a b : α<GOAL>a - b = a - min a b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c d a b : α<VAR>h : a ≤ b<GOAL>a - b = a - min a b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a✝ b✝ c d a b : α<VAR>h : b ≤ a<GOAL>a - b = a - min a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s₁ s₂ : Seq α<VAR>a : α<VAR>h : a ∈ s₁<GOAL>a ∈ s₁.append s₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s₁ s₂ : Seq α<VAR>a : α<VAR>h : a ∈ s₁<GOAL>∀ (b : α) (s' : Seq α), a = b ∨ a ∈ s'.append s₂ → a ∈ (cons b s').append s₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>X : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>e ∈ M.closure X ↔ ∀ (F : Set α), M.Flat F → X ⊆ F → e ∈ F
<VAR>X Y B : LightProfinite<VAR>f : X ⟶ B<VAR>g : Y ⟶ B<GOAL>pullback.snd f g = ((pullback.isLimit f g).conePointUniqueUpToIso (limit.isLimit (cospan f g))).hom ≫ Limits.pullback.snd f g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>h : 2 ≤ n<VAR>t : Finset α<VAR>ht : ⊥.IsNClique n t<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>m n : ℕ<VAR>s : Finset α<VAR>h : 2 ≤ n<VAR>t : Finset α<VAR>ht : ⊥.IsNClique n t<VAR>this : 2 ≤ 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>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<GOAL>Prime hζ.subOneIntegralPowerBasis.gen
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)<GOAL>‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)<VAR>s : HasSum (fun n => rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))<GOAL>‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<VAR>this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1)<VAR>s : HasSum (fun n => rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im)))<VAR>aux : Summable fun n => ‖cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖<GOAL>‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) / (1 - rexp (-π * τ.im))
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>u v : List (Symbol T N)<VAR>hyp : r.Rewrites u v<GOAL>∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜' E<VAR>inst✝⁴ : IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>g' : E →L[𝕜] F<VAR>h : HasFDerivAt f (restrictScalars 𝕜 f') x<VAR>H : restrictScalars 𝕜 f' = g'<GOAL>HasFDerivAt f f' x
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.12154<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : ∀ (u : U), Injective (φ.star u)<VAR>u v₁ : U<VAR>p₁ : Path u v₁<GOAL>∀ ⦃a₂ : PathStar u⦄, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨v₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨v₁, p₁⟩ = a₂
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.12154<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : ∀ (u : U), Injective (φ.star u)<VAR>u v₁ : U<VAR>h : True<GOAL>⟨u, Path.nil⟩ = ⟨u, Path.nil⟩
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.12154<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : ∀ (u : U), Injective (φ.star u)<VAR>u v₁ y₂ x₂ : U<VAR>p₂ : Path u x₂<VAR>e₂ : x₂ ⟶ y₂<VAR>h : φ.obj u = φ.obj y₂ ∧ HEq Path.nil ((φ.mapPath p₂).cons (φ.map e₂))<GOAL>⟨u, Path.nil⟩ = ⟨y₂, p₂.cons e₂⟩
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.12154<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : ∀ (u : U), Injective (φ.star u)<VAR>u v₁ x₁ y₁ : U<VAR>p₁ : Path u x₁<VAR>e₁ : x₁ ⟶ y₁<VAR>ih : ∀ ⦃a₂ : PathStar u⦄, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂<VAR>h : φ.obj y₁ = φ.obj u ∧ HEq ((φ.mapPath p₁).cons (φ.map e₁)) Path.nil<GOAL>⟨y₁, p₁.cons e₁⟩ = ⟨u, Path.nil⟩
<VAR>U : Type u_1<VAR>inst✝² : Quiver U<VAR>V : Type u_2<VAR>inst✝¹ : Quiver V<VAR>φ : U ⥤q V<VAR>W : Type ?u.12154<VAR>inst✝ : Quiver W<VAR>ψ : V ⥤q W<VAR>hφ : ∀ (u : U), Injective (φ.star u)<VAR>u v₁ x₁ y₁ : U<VAR>p₁ : Path u x₁<VAR>e₁ : x₁ ⟶ y₁<VAR>ih : ∀ ⦃a₂ : PathStar u⦄, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂<VAR>y₂ x₂ : U<VAR>p₂ : Path u x₂<VAR>e₂ : x₂ ⟶ y₂<VAR>h : φ.obj y₁ = φ.obj y₂ ∧ HEq ((φ.mapPath p₁).cons (φ.map e₁)) ((φ.mapPath p₂).cons (φ.map e₂))<GOAL>⟨y₁, p₁.cons e₁⟩ = ⟨y₂, p₂.cons e₂⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>f : ι → Filter α<VAR>inst✝ : Nonempty ι<VAR>hd : Directed (fun x x_1 => x ≥ x_1) f<GOAL>¬(iInf f).NeBot → ¬∀ (i : ι), (f i).NeBot
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<GOAL>Supermartingale (f - g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>inst✝¹ : Preorder E<VAR>inst✝ : CovariantClass E E (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>hf : Supermartingale f ℱ μ<VAR>hg : Submartingale g ℱ μ<GOAL>Supermartingale (f + -g) ℱ μ
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a.re * b.re + -1 * a.imI * b.imI + -1 * a.imJ * b.imJ - -1 * -1 * a.imK * b.imK = a.re * b.re - a.imI * b.imI - a.imJ * b.imJ - a.imK * b.imK
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>(span ℂ (range fourier)).topologicalClosure = ⊤
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<GOAL>(Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra).topologicalClosure = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x✝ y z : E<VAR>δ ε : ℝ<VAR>hε : 0 < ε<VAR>hδ : 0 < δ<VAR>x : E<GOAL>thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>hz : ‖z‖ = 1<GOAL>z.inv * z = 1
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp ⊤ (α × β)<GOAL>edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y) ≤ edist x y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : WithLp ⊤ (α × β)<GOAL>edist x y ≤ edist ((WithLp.equiv ⊤ (α × β)) x) ((WithLp.equiv ⊤ (α × β)) y)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ g✝ : X✝ ⟶ Y✝<VAR>h✝ : Y✝ ⟶ Z✝<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>h : X ⟶ Z<VAR>inst✝ : IsIso f<VAR>hh : IsIso (f ≫ g)<VAR>w : f ≫ g = h<VAR>this : IsIso (f ≫ g)<GOAL>IsIso g
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v : E<VAR>hv : v ∈ Kᗮ<GOAL>(reflection K) v = -v
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>inst✝² : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝¹ : FiberFunctor F<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : Nat.card ↑(F.obj X) = Nat.card ↑(F.obj Y)<VAR>this : IsIso (F.map f)<GOAL>IsIso f
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<GOAL>(Formula.iExs f φ).Realize v ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(Formula.iExs f φ).Realize v ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(let e := Classical.choice ⋯; (relabel (fun a => Sum.map id (⇑e) (f a)) φ).exs).Realize v ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(∃ xs, Realize φ (fun x => Sum.elim (fun x => v x) (fun x => xs (Fin.cast ⋯ ((Classical.choice ⋯) x))) (f x)) fun x => xs (natAdd (Classical.choose ⋯) x)) ↔ ∃ i, φ.Realize fun a => Sum.elim v i (f a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : Finite γ<VAR>f : α → β ⊕ γ<VAR>φ : L.Formula α<VAR>v : β → M<VAR>e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯<GOAL>(∀ (x : Fin (Classical.choose ⋯) → M), ¬Realize φ (fun x_1 => Sum.elim (fun x => v x) (fun x_2 => x (Fin.cast ⋯ ((Classical.choice ⋯) x_2))) (f x_1)) fun x_1 => x (natAdd (Classical.choose ⋯) x_1)) ↔ ∀ (x : γ → M), ¬φ.Realize fun a => Sum.elim v x (f a)