ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<VAR>f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart<VAR>_def_f_pos : f_pos = f.nnrealPart<VAR>f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart<VAR>_def_f_neg : f_neg = (-f).nnrealPart<VAR>tends_pos : Tendsto (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)<VAR>tends_neg : Tendsto (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_neg x) ∂↑μ).toReal)<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<VAR>f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart<VAR>_def_f_pos : f_pos = f.nnrealPart<VAR>f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart<VAR>_def_f_neg : f_neg = (-f).nnrealPart<VAR>tends_pos : Tendsto (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_pos x) ∂↑μ).toReal)<VAR>tends_neg : Tendsto (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f_neg x) ∂↑μ).toReal)<VAR>aux : ∀ (g : Ω →ᵇ ℝ≥0), (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) = fun i => (∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)).toReal<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))
<VAR>Ω : Type u_1<VAR>inst✝² : MeasurableSpace Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μ : FiniteMeasure Ω<VAR>h : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(f x) ∂↑μ))<VAR>f : Ω →ᵇ ℝ<VAR>f_pos : Ω →ᵇ ℝ≥0 := f.nnrealPart<VAR>_def_f_pos : f_pos = f.nnrealPart<VAR>f_neg : Ω →ᵇ ℝ≥0 := (-f).nnrealPart<VAR>_def_f_neg : f_neg = (-f).nnrealPart<VAR>aux : ∀ (g : Ω →ᵇ ℝ≥0), (ENNReal.toReal ∘ fun i => ∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)) = fun i => (∫⁻ (x : Ω), ↑(g x) ∂↑(μs i)).toReal<VAR>tends_pos : Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ))<VAR>tends_neg : Tendsto (fun i => ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_neg x) ∂↑μ))<GOAL>Tendsto (fun i => ∫ (x : Ω), ↑(f_pos x) ∂↑(μs i) - ∫ (x : Ω), ↑(f_neg x) ∂↑(μs i)) F (𝓝 (∫ (x : Ω), ↑(f_pos x) ∂↑μ - ∫ (x : Ω), ↑(f_neg x) ∂↑μ))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : CompleteSpace F<VAR>u : α → ℝ<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>g g' : α → 𝕜 → F<VAR>v : ℕ → α → ℝ<VAR>s : Set E<VAR>t : Set 𝕜<VAR>x₀ x✝ : E<VAR>y₀ y : 𝕜<VAR>N : ℕ∞<VAR>hu : Summable u<VAR>hf : ∀ (n : α), Differentiable 𝕜 (f n)<VAR>hf' : ∀ (n : α) (x : E), ‖fderiv 𝕜 (f n) x‖ ≤ u n<VAR>hf0 : Summable fun n => f n x₀<VAR>x : E<GOAL>fderiv 𝕜 (fun y => ∑' (n : α), f n y) x = ∑' (n : α), fderiv 𝕜 (f n) x
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 3
<VAR>α : Type u_1<VAR>inst✝³ : AddMonoidWithOne α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<GOAL>0 ≤ 2 + 1
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>hf : f ≠ 0<VAR>h : Splits (algebraMap F K) f<GOAL>Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : 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>inst✝² : (i : ι) → TopologicalSpace (σ i)<VAR>inst✝¹ : (k : κ) → TopologicalSpace (τ k)<VAR>inst✝ : TopologicalSpace X<VAR>f₁ : ι → κ<VAR>f₂ : (i : ι) → σ i → τ (f₁ i)<VAR>h : Injective f₁<GOAL>_root_.Embedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), _root_.Embedding (f₂ i)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsCompact (range f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>inst✝ : CompactSpace X<VAR>f : X → Y<VAR>hf : Continuous f<GOAL>IsCompact (f '' univ)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<GOAL>𝓝 (↑e.symm (↑e x)) = 𝓝 x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<GOAL>(trinomial k m n u v w).natTrailingDegree = k
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>i : ℕ<VAR>h : i ∈ (trinomial k m n u v w).support<GOAL>↑k ≤ ↑i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>i : ℕ<VAR>h : i ∈ {k, m, n}<GOAL>↑k ≤ ↑i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>hu : u ≠ 0<VAR>i : ℕ<VAR>h : i = k ∨ i = m ∨ i = n<GOAL>↑k ≤ ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>ι : Type u_1<VAR>I : ι → Ideal R<GOAL>Injective ⇑(quotientInfToPiQuotient I)
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n m✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>k m : ℕ<VAR>h : k ≠ m<VAR>x y : R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(C x * X ^ k + C y * X ^ m).support.card = 2
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j i : Fin n<GOAL>succAbove 0 i = i.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<VAR>s : Set α<VAR>hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<VAR>s : Set α<VAR>hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0<VAR>g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<VAR>s : Set α<VAR>hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0<VAR>g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a<VAR>g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a<GOAL>∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), Measurable (f n)<VAR>h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a<VAR>s : Set α<VAR>hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0<VAR>g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a<VAR>g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a<VAR>n : ℕ<VAR>a : α<GOAL>g n a ≤ g (n + 1) a
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>L R : ListBlank Γ<GOAL>(Tape.move Dir.left)^[n] (trTape' enc0 L R) = trTape' enc0 L.tail (ListBlank.cons L.head R)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<GOAL>(Tape.move Dir.left)^[n] (trTape' enc0 (ListBlank.cons a L) R) = trTape' enc0 (ListBlank.cons a L).tail (ListBlank.cons (ListBlank.cons a L).head R)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<GOAL>(Tape.move Dir.left)^[n] (Tape.mk' (ListBlank.append (enc a).toList.reverse (L.bind (fun x => (enc x).toList.reverse) ⋯)) (R.bind (fun x => (enc x).toList) ⋯)) = Tape.mk' (L.bind (fun x => (enc x).toList.reverse) ⋯) (ListBlank.append (enc a).toList (R.bind (fun x => (enc x).toList) ⋯))
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<GOAL>∀ {L' R' : ListBlank Bool} {l₁ l₂ : List Bool}, (enc a).toList = l₁.reverseAux l₂ → (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂ R')) = Tape.mk' L' (ListBlank.append (enc a).toList R')
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<VAR>L'✝ R'✝ : ListBlank Bool<VAR>b : Bool<VAR>l₁ : List Bool<VAR>IH : ∀ {l₂ : List Bool}, (enc a).toList = l₁.reverseAux l₂ → (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) = Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)<VAR>l₂ : List Bool<VAR>e : (enc a).toList = (b :: l₁).reverseAux l₂<GOAL>(Tape.move Dir.left)^[(b :: l₁).length] (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) = Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<VAR>L'✝ R'✝ : ListBlank Bool<VAR>b : Bool<VAR>l₁ : List Bool<VAR>IH : ∀ {l₂ : List Bool}, (enc a).toList = l₁.reverseAux l₂ → (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) = Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)<VAR>l₂ : List Bool<VAR>e : (enc a).toList = (b :: l₁).reverseAux l₂<GOAL>(Tape.move Dir.left)^[l₁.length] (Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝))) = Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)
<VAR>Γ : Type u_1<VAR>inst✝² : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_3<VAR>inst✝ : Inhabited σ<VAR>n : ℕ<VAR>enc : Γ → Vector Bool n<VAR>dec : Vector Bool n → Γ<VAR>enc0 : enc default = Vector.replicate n false<VAR>M : Λ → Stmt₁<VAR>R : ListBlank Γ<VAR>a : Γ<VAR>L : ListBlank Γ<VAR>L'✝ R'✝ : ListBlank Bool<VAR>b : Bool<VAR>l₁ : List Bool<VAR>IH : ∀ {l₂ : List Bool}, (enc a).toList = l₁.reverseAux l₂ → (Tape.move Dir.left)^[l₁.length] (Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append l₂ R'✝)) = Tape.mk' L'✝ (ListBlank.append (enc a).toList R'✝)<VAR>l₂ : List Bool<VAR>e : (enc a).toList = (b :: l₁).reverseAux l₂<GOAL>Tape.move Dir.left (Tape.mk' (ListBlank.append (b :: l₁) L'✝) (ListBlank.append l₂ R'✝)) = Tape.mk' (ListBlank.append l₁ L'✝) (ListBlank.append (b :: l₂) R'✝)
<VAR>a b c : ℤ<GOAL>a ≠ 0 ∧ b ≠ 0 ∧ a ^ 4 + b ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2
<VAR>a b c : ℤ<GOAL>a ≠ 0 ∧ b ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2 ↔ b ≠ 0 ∧ a ≠ 0 ∧ b ^ 4 + a ^ 4 = c ^ 2
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<GOAL>gauge t (gaugeRescale s t x) = gauge s x
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<GOAL>gauge t (gaugeRescale s t 0) = gauge s 0
<VAR>E : Type u_1<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T1Space E<VAR>s t : Set E<VAR>hta : Absorbent ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ≠ 0<GOAL>gauge t (gaugeRescale s t x) = gauge s x
<VAR>m n✝ n : ℕ<VAR>hn : Odd n<VAR>a : ZMod n<GOAL>a + a = 0 ↔ a = 0
<VAR>m n✝ n : ℕ<VAR>hn : Nat.Coprime 2 n<VAR>a : ZMod n<GOAL>a + a = 0 ↔ a = 0
<VAR>f : Bool → Bool → Bool<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>(if n = 0 then if f false true = true then m else 0 else if m = 0 then if f true false = true then n else 0 else let n' := n / 2; let m' := m / 2; let b₁ := n % 2 = 1; let b₂ := m % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))
<VAR>f : Bool → Bool → Bool<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<VAR>mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd<GOAL>(if n = 0 then if f false true = true then m else 0 else if m = 0 then if f true false = true then n else 0 else let n' := n / 2; let m' := m / 2; let b₁ := n % 2 = 1; let b₂ := m % 2 = 1; let r := bitwise f n' m'; if f (decide b₁) (decide b₂) = true then r + r + 1 else r + r) = bit (f n.bodd m.bodd) (bitwise f (n / 2) (m / 2))
<VAR>f : Bool → Bool → Bool<VAR>n m : ℕ<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<VAR>mod_two_iff_bod : ∀ (x : ℕ), decide (x % 2 = 1) = x.bodd<GOAL>(if f n.bodd m.bodd = true then bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2) + 1 else bitwise f (n / 2) (m / 2) + bitwise f (n / 2) (m / 2)) = (if f n.bodd m.bodd = true then fun x => x + x + 1 else fun x => x + x) (bitwise f (n / 2) (m / 2))
<VAR>D : GlueData<VAR>i j : D.J<VAR>x : ↑↑(D.U i).toPresheafedSpace<VAR>y : ↑↑(D.U j).toPresheafedSpace<GOAL>(D.ι i).val.base x = (D.ι j).val.base y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩
<VAR>D : GlueData<VAR>i j : D.J<VAR>x : ↑↑(D.U i).toPresheafedSpace<VAR>y : ↑↑(D.U j).toPresheafedSpace<GOAL>(D.ι i).val.base x = (D.ι j).val.base y ↔ (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) x = (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j) y
<VAR>D : GlueData<VAR>i j : D.J<VAR>x : ↑↑(D.U i).toPresheafedSpace<VAR>y : ↑↑(D.U j).toPresheafedSpace<GOAL>(D.ι i).val.base x = (D.ι j).val.base y ↔ D.isoCarrier.inv ((D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) x) = D.isoCarrier.inv ((D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j) y)
<VAR>D : GlueData<VAR>i j : D.J<VAR>x : ↑↑(D.U i).toPresheafedSpace<VAR>y : ↑↑(D.U j).toPresheafedSpace<GOAL>Mono D.isoCarrier.inv
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ x : M<GOAL>HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ x : M<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I) (↑(extChartAt I x) x)
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ x : M<VAR>this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I) (↑(extChartAt I x) x)
<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>inst✝ : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x✝ x : M<VAR>this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y<GOAL>(↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = id (↑(extChartAt I x) x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g✝ : Perm α<VAR>x y : α<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>hy : f y ≠ y<VAR>g : α<VAR>hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y<VAR>a : ℤ<VAR>ha : (f ^ a) g = x<VAR>b : ℤ<VAR>hb : (f ^ b) g = y<GOAL>(f ^ (b - a)) x = y
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<GOAL>IsIntegral ℤ μ
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝ : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<GOAL>(X ^ n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (X ^ n - 1) = 0
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>U : Set X<GOAL>Perfect U ↔ U = derivedSet U
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this : DecidableEq G<GOAL>∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this : DecidableEq G<VAR>R₀ : Set G<VAR>hR : R₀ ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R₀<GOAL>∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this✝ : DecidableEq G<VAR>R₀ : Set G<VAR>hR : R₀ ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R₀<VAR>this : Fintype ↑R₀<VAR>R : Finset G := R₀.toFinset<GOAL>∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this✝ : DecidableEq G<VAR>R₀ : Set G<VAR>hR1 : 1 ∈ R₀<VAR>this : Fintype ↑R₀<VAR>R : Finset G := R₀.toFinset<VAR>hR : ↑R ∈ rightTransversals ↑H<GOAL>∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this✝ : DecidableEq G<VAR>R₀ : Set G<VAR>this : Fintype ↑R₀<VAR>R : Finset G := R₀.toFinset<VAR>hR : ↑R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<GOAL>∃ T, T.card ≤ H.index * S.card ∧ closure ↑T = ⊤
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this✝ : DecidableEq G<VAR>R₀ : Set G<VAR>this : Fintype ↑R₀<VAR>R : Finset G := R₀.toFinset<VAR>hR : ↑R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<GOAL>(Finset.image (fun g => ⟨g * (↑(toFun hR g))⁻¹, ⋯⟩) (R * S)).card ≤ H.index * S.card
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>R✝ S✝ : Set G<VAR>inst✝ : H.FiniteIndex<VAR>S : Finset G<VAR>hS : closure ↑S = ⊤<VAR>this✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>this✝ : DecidableEq G<VAR>R₀ : Set G<VAR>this : Fintype ↑R₀<VAR>R : Finset G := R₀.toFinset<VAR>hR : ↑R ∈ rightTransversals ↑H<VAR>hR1 : 1 ∈ R<GOAL>R.card = H.index