ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n))) ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))<GOAL>C ↑(p ^ (n + 1)) ∣ (bind₁ fun b => (rename fun i => (b, i)) (W_ ℤ (n + 1))) Φ - ∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n))) ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))<GOAL>(bind₁ fun i => (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((rename fun i_1 => (i, i_1)) (W_ ℤ (n + 1)))) ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((map (Int.castRingHom ℚ)) Φ) m<VAR>key : (bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n))) ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n))<GOAL>(bind₁ fun i => (rename fun i_1 => (i, i_1)) ((expand p) (W_ (ZMod (p ^ (n + 1))) n))) ((map (Int.castRingHom (ZMod (p ^ (n + 1))))) Φ) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(map (Int.castRingHom (ZMod (p ^ (n + 1))))) ((bind₁ fun i => (expand p) (wittStructureInt p Φ i)) (W_ ℤ n)) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (∑ i ∈ Finset.range (n + 1), C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n + 1 - i))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>∀ x ∈ Finset.range (n + 1), (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ x * (expand p) (wittStructureInt p Φ x) ^ p ^ (n - x)) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ x) * wittStructureInt p Φ x ^ p ^ (n + 1 - x))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<GOAL>(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>(map (Int.castRingHom (ZMod (p ^ (n + 1))))) (↑p ^ k * (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k)) = (map (Int.castRingHom (ZMod (p ^ (n + 1))))) (C (↑p ^ k) * wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<GOAL>↑(p ^ (n + 1)) ∣ ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑(p ^ (n + 1)) ∣ ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑(p ^ k * p ^ (n - k + 1)) ∣ ↑(p ^ k) * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑p ^ k * ↑p ^ (n - k + 1) ∣ ↑p ^ k * ((expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ p ^ (n + 1 - k)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - wittStructureInt p Φ k ^ (p * p ^ (n - k))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑p ^ (n - k + 1) ∣ (expand p) (wittStructureInt p Φ k) ^ p ^ (n - k) - (wittStructureInt p Φ k ^ p) ^ p ^ (n - k)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n k : ℕ<VAR>hk : k ≤ n<VAR>this : p ^ (n + 1) = p ^ k * p ^ (n - k + 1)<GOAL>↑p ∣ (expand p) (wittStructureInt p Φ k) - wittStructureInt p Φ k ^ p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<GOAL>∃ r, ∀ (i : ℕ), abv (f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>i : ℕ<VAR>h : ∀ j ≥ i, abv (f j - f i) < 1<GOAL>∃ r, ∀ (i : ℕ), abv (f i) < r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>i : ℕ<VAR>h : ∀ j ≥ i, abv (f j - f i) < 1<VAR>R : ℕ → α := Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>hR : R = Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i<VAR>j : ℕ<GOAL>abv (f j) < R i + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>i : ℕ<VAR>h : ∀ j ≥ i, abv (f j - f i) < 1<VAR>R : ℕ → α := Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>hR : R = Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i<VAR>j : ℕ<VAR>hji : j ≤ i<GOAL>abv (f j) < R i + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : Ring β<VAR>abv : β → α<VAR>inst✝ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>hf : IsCauSeq abv f<VAR>i : ℕ<VAR>h : ∀ j ≥ i, abv (f j - f i) < 1<VAR>R : ℕ → α := Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>hR : R = Nat.rec (abv (f 0)) fun i c => max c (abv (f i.succ))<VAR>this : ∀ (i j : ℕ), j ≤ i → abv (f j) ≤ R i<VAR>j : ℕ<VAR>hij : i ≤ j<GOAL>abv (f j) < R i + 1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>F : Fintype { x // x ∈ s }<VAR>h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x<GOAL>∏ a ∈ s, f a = ∏ a : { x // x ∈ s }, f ↑a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>f : α → β<VAR>F : Fintype { x // x ∈ s }<VAR>h : ∀ (x : α), x ∈ s ↔ (fun x => x ∈ s) x<GOAL>∏ i : { x // x ∈ s }, f ↑i = ∏ a : { x // x ∈ s }, f ↑a
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>p q : ℕ<VAR>inst✝ : ExpChar R p<VAR>f : R[X]<VAR>n✝ : ℕ<VAR>n_ih : map (frobenius R p ^ n✝) ((expand R (p ^ n✝)) f) = f ^ p ^ n✝<GOAL>f ^ p ^ (n✝ + 1) = map (frobenius R p ^ (n✝ + 1)) ((expand R (p ^ (n✝ + 1))) f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<GOAL>MeasurableSet {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<GOAL>MeasurableSet {p | p.2 ∈ D (f p.1) K}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<GOAL>MeasurableSet {p | ∀ (i : ℕ), ∃ i_1, ∀ i_2 ≥ i_1, ∀ i_4 ≥ i_1, p.2 ∈ B (f p.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_4) ((1 / 2) ^ i)}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<GOAL>MeasurableSet (⋂ i, ⋃ i_1, ⋂ i_2, ⋂ (_ : i_2 ≥ i_1), ⋂ i_3, ⋂ (_ : i_3 ≥ i_1), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_2) ((1 / 2) ^ i_3) ((1 / 2) ^ i)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝ : ℕ<GOAL>MeasurableSet (⋃ i, ⋂ i_1, ⋂ (_ : i_1 ≥ i), ⋂ i_2, ⋂ (_ : i_2 ≥ i), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i_1) ((1 / 2) ^ i_2) ((1 / 2) ^ x✝)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝¹ x✝ : ℕ<GOAL>MeasurableSet (⋂ i, ⋂ (_ : i ≥ x✝), ⋂ i_1, ⋂ (_ : i_1 ≥ x✝), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ i) ((1 / 2) ^ i_1) ((1 / 2) ^ x✝¹)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝² x✝¹ x✝ : ℕ<GOAL>MeasurableSet (⋂ (_ : x✝ ≥ x✝¹), ⋂ i, ⋂ (_ : i ≥ x✝¹), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝) ((1 / 2) ^ i) ((1 / 2) ^ x✝²)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝³ x✝² x✝¹ : ℕ<VAR>x✝ : x✝¹ ≥ x✝²<GOAL>MeasurableSet (⋂ i, ⋂ (_ : i ≥ x✝²), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝¹) ((1 / 2) ^ i) ((1 / 2) ^ x✝³)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝⁴ x✝³ x✝² : ℕ<VAR>x✝¹ : x✝² ≥ x✝³<VAR>x✝ : ℕ<GOAL>MeasurableSet (⋂ (_ : x✝ ≥ x✝³), {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝²) ((1 / 2) ^ x✝) ((1 / 2) ^ x✝⁴)})
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝⁵ x✝⁴ x✝³ : ℕ<VAR>x✝² : x✝³ ≥ x✝⁴<VAR>x✝¹ : ℕ<VAR>x✝ : x✝¹ ≥ x✝⁴<GOAL>MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace α<VAR>inst✝ : OpensMeasurableSpace E<VAR>f : α → E → F<VAR>K✝ : Set (E →L[𝕜] F)<VAR>hf : Continuous (Function.uncurry f)<VAR>K : Set (E →L[𝕜] F)<VAR>hK : IsComplete K<VAR>this✝ : {p | DifferentiableAt 𝕜 (f p.1) p.2 ∧ fderiv 𝕜 (f p.1) p.2 ∈ K} = {p | p.2 ∈ D (f p.1) K}<VAR>x✝⁵ x✝⁴ x✝³ : ℕ<VAR>x✝² : x✝³ ≥ x✝⁴<VAR>x✝¹ : ℕ<VAR>x✝ : x✝¹ ≥ x✝⁴<VAR>this : ProperSpace E<GOAL>MeasurableSet {x | x.2 ∈ B (f x.1) K ((1 / 2) ^ x✝³) ((1 / 2) ^ x✝¹) ((1 / 2) ^ x✝⁵)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<GOAL>NoetherianSpace ↑s ↔ ∀ t ⊆ s, IsCompact t
<VAR>s t : Set ℝ<GOAL>frontier (s ×ℂ t) = closure s ×ℂ frontier t ∪ frontier s ×ℂ closure t
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε✝ : ℝ<VAR>s t : Set α<VAR>x : α<VAR>ε : ℝ≥0<GOAL>EMetric.diam (cthickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝¹ : α<VAR>ε : ℝ≥0<VAR>x : α<VAR>hx : x ∈ cthickening (↑ε) s<VAR>y : α<VAR>hy : y ∈ cthickening (↑ε) s<VAR>δ : ℝ≥0<VAR>hδ : 0 < δ<VAR>x✝ : EMetric.diam s + 2 * ↑ε < ⊤<GOAL>edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝¹ : α<VAR>ε : ℝ≥0<VAR>x : α<VAR>hx : infEdist x s ≤ ↑ε<VAR>y : α<VAR>hy : infEdist y s ≤ ↑ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < δ<VAR>x✝ : EMetric.diam s + 2 * ↑ε < ⊤<GOAL>edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝¹ : α<VAR>ε : ℝ≥0<VAR>x : α<VAR>hx : infEdist x s ≤ ↑ε<VAR>y : α<VAR>hy : infEdist y s ≤ ↑ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < δ<VAR>x✝ : EMetric.diam s + 2 * ↑ε < ⊤<VAR>hε : ↑ε < ↑ε + ↑δ<GOAL>edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝¹ : α<VAR>ε : ℝ≥0<VAR>x y : α<VAR>hy : infEdist y s ≤ ↑ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < δ<VAR>x✝ : EMetric.diam s + 2 * ↑ε < ⊤<VAR>hε : ↑ε < ↑ε + ↑δ<VAR>hx : infEdist x s < ↑ε + ↑δ<GOAL>edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε✝ : ℝ<VAR>s t : Set α<VAR>x✝¹ : α<VAR>ε : ℝ≥0<VAR>x y : α<VAR>hy : infEdist y s ≤ ↑ε<VAR>δ : ℝ≥0<VAR>hδ : 0 < δ<VAR>x✝ : EMetric.diam s + 2 * ↑ε < ⊤<VAR>hε : ↑ε < ↑ε + ↑δ<VAR>hx : infEdist x s < ↑ε + ↑δ<VAR>x' : α<VAR>hx' : x' ∈ s<VAR>hxx' : edist x x' < ↑ε + ↑δ<GOAL>edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>c : R<VAR>h : c • x ∈ (mkSpanSingleton' x y H).domain<GOAL>Classical.choose ⋯ • y = c • y
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>c : R<VAR>h : c • x ∈ (mkSpanSingleton' x y H).domain<GOAL>(Classical.choose ⋯ - c) • y = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>c : R<VAR>h : c • x ∈ (mkSpanSingleton' x y H).domain<GOAL>(Classical.choose ⋯ - c) • x = 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>x : E<VAR>y : F<VAR>H : ∀ (c : R), c • x = 0 → c • y = 0<VAR>c : R<VAR>h : c • x ∈ (mkSpanSingleton' x y H).domain<GOAL>Classical.choose ⋯ • x = c • x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' : List α<GOAL>(t :: is ++ ts).permutationsAux is' = map (fun x => x ++ ts) ((t :: is).permutationsAux is') ++ ts.permutationsAux ((t :: is).reverse ++ is')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' : List α<GOAL>(is'.permutations.bind fun y => (permutationsAux2 t (is ++ ts) [] y id).2) ++ (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: is')) = (is'.permutations.bind fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2) ++ (map (fun x => x ++ ts) (is.permutationsAux (t :: is')) ++ ts.permutationsAux (is.reverse ++ t :: ([] ++ is')))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' : List α<GOAL>(fun y => (permutationsAux2 t (is ++ ts) [] y id).2) = fun a => map (fun x => x ++ ts) (permutationsAux2 t is [] a id).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ts : List α<VAR>t : α<VAR>is : List α<VAR>ih : ∀ (is' : List α), (is ++ ts).permutationsAux is' = map (fun x => x ++ ts) (is.permutationsAux is') ++ ts.permutationsAux (is.reverse ++ is')<VAR>is' x✝ : List α<GOAL>(permutationsAux2 t (is ++ ts) [] x✝ id).2 = map (fun x => x ++ ts) (permutationsAux2 t is [] x✝ id).2