ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℂ E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℂ F<VAR>inst✝ : Nontrivial E<VAR>f : E → F<VAR>U : Set E<VAR>hU : Bornology.IsBounded U<VAR>C : ℝ<VAR>hC : ∀ z ∈ frontier U, ‖f z‖ ≤ C<VAR>z : E<VAR>hz : z ∈ U<VAR>w : E<VAR>hne : w ≠ z<VAR>e : ℂ → E := ⇑(lineMap z w)<VAR>hde : Differentiable ℂ e<VAR>hL : AntilipschitzWith (nndist z w)⁻¹ e<VAR>hd : DiffContOnCl ℂ (f ∘ e) (e ⁻¹' U)<VAR>h₀ : 0 ∈ e ⁻¹' U<VAR>ζ : ℂ<VAR>hζU : ζ ∈ frontier (e ⁻¹' U)<VAR>hζ : IsMaxOn (norm ∘ f ∘ e) (closure (e ⁻¹' U)) ζ<GOAL>‖f z‖ ≤ C
<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>s✝ : Set α<VAR>hs✝ : MeasurableSet s✝<VAR>hμs✝ : μ s✝ ≠ ⊤<VAR>c✝ : E<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>c : E<GOAL>↑↑(indicatorConstLp p ⋯ ⋯ c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c)
<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>s✝ : Set α<VAR>hs✝ : MeasurableSet s✝<VAR>hμs✝ : μ s✝ ≠ ⊤<VAR>c✝ : E<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>c : E<GOAL>((s ∪ t).indicator fun x => c) =ᶠ[ae μ] ↑↑(indicatorConstLp p hs hμs c) + ↑↑(indicatorConstLp p ht hμt c)
<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>s✝ : Set α<VAR>hs✝ : MeasurableSet s✝<VAR>hμs✝ : μ s✝ ≠ ⊤<VAR>c✝ : E<VAR>s t : Set α<VAR>hs : MeasurableSet s<VAR>ht : MeasurableSet t<VAR>hμs : μ s ≠ ⊤<VAR>hμt : μ t ≠ ⊤<VAR>hst : s ∩ t = ∅<VAR>c : E<GOAL>((s ∪ t).indicator fun x => c) =ᶠ[ae μ] fun x => s.indicator (fun x => c) x + t.indicator (fun x => c) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hs : s.einfsep < ⊤<GOAL>s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>hs : s.einfsep < ⊤<VAR>w✝¹ : α<VAR>hx : w✝¹ ∈ s<VAR>w✝ : α<VAR>hy : w✝ ∈ s<VAR>hxy : w✝¹ ≠ w✝<VAR>right✝ : edist w✝¹ w✝ < ⊤<GOAL>s.Nontrivial
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<GOAL>((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hdp : (p ^ 2).degree = 2 • p.degree<GOAL>((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hdp : (p ^ 2).degree = 2 • p.degree<VAR>hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1<GOAL>((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hdp : (p ^ 2).degree = 2 • p.degree<VAR>hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1<VAR>hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3<GOAL>((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hdp : (p ^ 2).degree = 2 • p.degree<VAR>hdpq : (p * q * (C W.a₁ * X + C W.a₃)).degree ≤ p.degree + q.degree + 1<VAR>hdq : (q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = 2 • q.degree + 3<GOAL>(p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)).degree = max (2 • p.degree) (2 • q.degree + 3)
<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 : β<GOAL>f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t
<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 : β<GOAL>f '' s = t → SurjOn f s t ∧ MapsTo f s t
<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₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : AddMonoid β<VAR>f : ℕ →+ β<VAR>n : ℕ<GOAL>f n = n • f 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Semifield R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : HasContinuousInv₀ R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>a : Aˣ<VAR>n : ℤ<VAR>ha : autoParam (p ↑a) _auto✝<GOAL>cfc (fun x => x ^ n) ↑a = ↑(a ^ n)
<VAR>f : Bool → Bool → Bool<VAR>n : ℕ<GOAL>(if n = 0 then if f false true = true then 0 else 0 else if 0 = 0 then if f true false = true then n else 0 else let n' := n / 2; let m' := 0 / 2; let b₁ := n % 2 = 1; let b₂ := 0 % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = if f true false = true then n else 0
<VAR>f : Bool → Bool → Bool<VAR>n : ℕ<GOAL>n = 0 → 0 = if f true false = true then n else 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hg : ∀ i ∈ s, 0 ≤ g i<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>n : ℕ<GOAL>a + ↑n = b + ↑n ↔ a = b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>h : conjugatesOf a = conjugatesOf b<GOAL>IsConj a b
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Monoid α<VAR>a b : α<VAR>h : conjugatesOf a = conjugatesOf b<VAR>ha : b ∈ conjugatesOf b<GOAL>IsConj a b
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M<VAR>n : ℕ<VAR>h : Module.rank R M = ↑n<VAR>a✝ : Nontrivial R<GOAL>Finite R M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M<VAR>n : ℕ<VAR>h : Module.rank R M = ↑n<VAR>a✝ : Nontrivial R<VAR>ι : Type v<VAR>b : Basis ι R M<GOAL>Finite R M
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι✝ : Type w<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Free R M<VAR>n : ℕ<VAR>h : Module.rank R M = ↑n<VAR>a✝ : Nontrivial R<VAR>ι : Type v<VAR>b : Basis ι R M<VAR>this : _root_.Finite ι<GOAL>Finite R M
<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Algebra K L<VAR>inst✝⁴ : Algebra F K<VAR>inst✝³ : Algebra F L<VAR>inst✝² : IsScalarTower F K L<VAR>f g : F[X]<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<VAR>inst✝¹ : IsSplittingField F K f<VAR>inst✝ : IsSplittingField K L (Polynomial.map (algebraMap F K) g)<GOAL>Algebra.adjoin F ((f * g).rootSet L) = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b<VAR>ha : a ∈ Ici a<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<GOAL>ContinuousWithinAt f (Ici a) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<VAR>b : β<VAR>hb : b < f a<GOAL>∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : OrderTopology α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>h_mono : StrictMonoOn f s<VAR>hs : s ∈ 𝓝[≥] a<VAR>hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b<VAR>ha : a ∈ Ici a<VAR>has : a ∈ s<VAR>b : β<VAR>hb : b > f a<GOAL>∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v (y - x) < v x<GOAL>v y = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v (y - x) < v x<VAR>this : v (y - x + x) = max (v (y - x)) (v x)<GOAL>v y = v x
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>h : v (y - x) < v x<VAR>this : v (y - x + x) = v x<GOAL>v y = v x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<VAR>hg : g.NeBot<VAR>s : Set β<VAR>hs : s ∈ g<GOAL>(fun x => 0 • x) '' s ∈ 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : SMulWithZero α β<VAR>f : Filter α<VAR>g : Filter β<VAR>hg : g.NeBot<VAR>s : Set β<VAR>hs : s ∈ g<GOAL>{0} ∈ 0
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hq : 0 ≤ q<GOAL>ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hq : 0 ≤ q<VAR>h : p ≤ q<GOAL>ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hq : 0 ≤ q<VAR>h : q ≤ p<GOAL>ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>hq : 0 ≤ q<VAR>h : q ≤ p<GOAL>ENNReal.ofReal (p - q) + ENNReal.ofReal q = ENNReal.ofReal p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x y : 𝕎 R<GOAL>WittVector.ghostFun (x + y) = WittVector.ghostFun x + WittVector.ghostFun y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<GOAL>IsConj σ τ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<GOAL>∀ (x : α) (hx : x ∈ ↑σ.support), ↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨σ x, ⋯⟩) = τ ↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨x, hx⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>x : α<VAR>hx : x ∈ ↑σ.support<GOAL>↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨σ x, ⋯⟩) = τ ↑((hσ.zpowersEquivSupport.symm.trans ((zpowersEquivZPowers ⋯).trans hτ.zpowersEquivSupport)) ⟨x, hx⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>x : α<VAR>hx : x ∈ ↑σ.support<GOAL>↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ x, ⋯⟩))) = τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨x, hx⟩)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ ((σ ^ n) (Classical.choose hσ)), ⋯⟩))) = τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), hx⟩)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ ((σ ^ n) (Classical.choose hσ)), ⋯⟩))) = τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) ⟨σ ^ n, ⋯⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨(σ ^ (n + 1)) (Classical.choose hσ), ⋯⟩))) = τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) ⟨σ ^ n, ⋯⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) ⟨σ ^ (n + 1), ⋯⟩)) = τ ↑(hτ.zpowersEquivSupport ((zpowersEquivZPowers ⋯) ⟨σ ^ n, ⋯⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>↑⟨(τ ^ (n + 1)) (Classical.choose hτ), ⋯⟩ = τ ↑(hτ.zpowersEquivSupport ⟨τ ^ n, ⋯⟩)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ τ : Perm α<VAR>hσ : σ.IsCycle<VAR>hτ : τ.IsCycle<VAR>h : σ.support.card = τ.support.card<VAR>n : ℕ<VAR>hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support<GOAL>τ ((τ ^ n) (Classical.choose hτ)) = τ ↑(hτ.zpowersEquivSupport ⟨τ ^ n, ⋯⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹³ : TopologicalSpace α<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : OpensMeasurableSpace α<VAR>inst✝¹⁰ : TopologicalSpace β<VAR>inst✝⁹ : MeasurableSpace β<VAR>inst✝⁸ : OpensMeasurableSpace β<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : TopologicalSpace γ₂<VAR>inst✝³ : MeasurableSpace γ₂<VAR>inst✝² : BorelSpace γ₂<VAR>inst✝¹ : MeasurableSpace δ<VAR>inst✝ : R1Space γ<VAR>K s : Set γ<VAR>hK : IsCompact K<VAR>hs : MeasurableSet s<VAR>hKs : K ⊆ s<GOAL>closure K ⊆ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹³ : TopologicalSpace α<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : OpensMeasurableSpace α<VAR>inst✝¹⁰ : TopologicalSpace β<VAR>inst✝⁹ : MeasurableSpace β<VAR>inst✝⁸ : OpensMeasurableSpace β<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : TopologicalSpace γ₂<VAR>inst✝³ : MeasurableSpace γ₂<VAR>inst✝² : BorelSpace γ₂<VAR>inst✝¹ : MeasurableSpace δ<VAR>inst✝ : R1Space γ<VAR>K s : Set γ<VAR>hK : IsCompact K<VAR>hs : MeasurableSet s<VAR>hKs : K ⊆ s<GOAL>∀ i ∈ K, {y | Inseparable i y} ⊆ s
<VAR>x : ℝ<GOAL>↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
<VAR>x : ℝ<VAR>h : x ≤ 0<GOAL>↑x = ↑↑x.toNNReal - ↑↑(-x).toNNReal
<VAR>q : ℚ<VAR>x y : ℝ<GOAL>x + y ∉ Set.range Rat.cast → x ∉ Set.range Rat.cast ∨ y ∉ Set.range Rat.cast
<VAR>q : ℚ<VAR>x y : ℝ<GOAL>x ∈ Set.range Rat.cast ∧ y ∈ Set.range Rat.cast → x + y ∈ Set.range Rat.cast
<VAR>q rx ry : ℚ<GOAL>↑rx + ↑ry ∈ Set.range Rat.cast
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℝ → ℝ<VAR>a b : ℝ<GOAL>⨍ (x : ℝ) in a..b, f x = (∫ (x : ℝ) in a..b, f x) / (b - a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<GOAL>fiber none = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<GOAL>∀ (x : Perm α), x ∉ fiber none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hyp : f ∈ fiber none<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>hyp : ∃ F ∈ derangements (Option α), F none = none ∧ removeNone F = f<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f✝ g✝ : X → Y<VAR>f g : (i : ι) → π i<GOAL>(f ~ᵢ g) ↔ ∀ (i : ι), f i ~ᵢ g i
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Splits (algebraMap F K) (minpoly F α)<GOAL>Fintype.card (↥F⟮α⟯ →ₐ[F] K) = (minpoly F α).natDegree
<VAR>F : Type u_1<VAR>inst✝⁴ : Field F<VAR>E : Type u_2<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>h : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Splits (algebraMap F K) (minpoly F α)<GOAL>(minpoly F α).Separable
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K U : Set X<VAR>hK : IsCompact K<VAR>hU : U ∈ 𝓝ˢ K<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K U : Set X<VAR>hK : IsCompact K<VAR>hU : U ∈ 𝓝ˢ K<VAR>hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K U : Set X<VAR>hK : IsCompact K<VAR>hU : U ∈ 𝓝ˢ K<VAR>hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)<VAR>V : Set X<VAR>hVo : IsOpen V<VAR>hKV : K ⊆ V<VAR>W : Set X<VAR>hVW : Disjoint V W<VAR>hW : IsOpen W<VAR>hUW : Uᶜ ⊆ W<GOAL>∃ V, IsOpen V ∧ K ⊆ V ∧ closure V ⊆ U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : RegularSpace X<VAR>x : X<VAR>s K U : Set X<VAR>hK : IsCompact K<VAR>hU : U ∈ 𝓝ˢ K<VAR>hd : Disjoint (𝓝ˢ K) (𝓝ˢ Uᶜ)<VAR>V : Set X<VAR>hVo : IsOpen V<VAR>hKV : K ⊆ V<VAR>W : Set X<VAR>hVW : Disjoint V W<VAR>hW : IsOpen W<VAR>hUW : Uᶜ ⊆ W<GOAL>closure V ⊆ Wᶜ
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>x : Lifts F E K<VAR>s : E<VAR>h1 : IsIntegral F s<VAR>h2 : Splits (algebraMap F K) (minpoly F s)<GOAL>Splits (x.emb.comp (algebraMap F ↥x.carrier)) (minpoly F s)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Preorder α<VAR>inst✝² : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>x y : α<GOAL>cmpLE x y = cmp x y
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Preorder α<VAR>inst✝² : IsTotal α fun x x_1 => x ≤ x_1<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>x y : α<VAR>xy : ¬x ≤ y<VAR>yx : ¬y ≤ x<GOAL>False
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>a b : α<VAR>h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b<GOAL>a ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>a b : α<VAR>h : ∀ (c : α), IsAtom c → c ≤ a → c ≤ b<GOAL>sSup {a_1 | IsAtom a_1 ∧ a_1 ≤ a} ≤ sSup {a | IsAtom a ∧ a ≤ b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>s t : Set α<VAR>a : α<VAR>h1 : s ∈ 𝓝 a<VAR>h2 : t ∈ 𝓝[s] a<GOAL>t ∈ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>s t : Set α<VAR>a : α<VAR>h1 : s ∈ 𝓝 a<VAR>h2 : t ∈ 𝓝[s] a<VAR>w✝ : Set α<VAR>Hw : w✝ ∈ 𝓝 a<VAR>hw : w✝ ∩ s ⊆ t<GOAL>t ∈ 𝓝 a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>k : ℕ<VAR>s : Set ℕ := {k | x ^ k = 0}<GOAL>nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : MonoidWithZero R<VAR>k : ℕ<VAR>s : Set ℕ := {k | x ^ k = 0}<VAR>this : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s<GOAL>nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a b : α<VAR>s : Finset α<GOAL>(∃ a, s = {a}) ↔ ∃! a, a ∈ s
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(enumFrom n l).unzip = (range' n l.length, l)
<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>a✝ b✝ : ℚ<VAR>h : dist a✝ b✝ < ε<GOAL>dist (-a✝) (-b✝) < ε
<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>a✝ b✝ : ℚ<VAR>h : dist b✝ a✝ < ε<GOAL>dist (-a✝) (-b✝) < ε