ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)<GOAL>HasStrictFDerivAt (fun x => rexp (log x.1 * x.2) * cos (x.2 * π)) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)<VAR>e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'<GOAL>(p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ = rexp (log p.1 * p.2) • -sin (p.2 * π) • π • ContinuousLinearMap.snd ℝ ℝ ℝ + cos (p.2 * π) • rexp (log p.1 * p.2) • (log p.1 • ContinuousLinearMap.snd ℝ ℝ ℝ + p.2 • p.1⁻¹ • ContinuousLinearMap.fst ℝ ℝ ℝ)
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)<VAR>e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'<GOAL>(p.2 * (p.1 ^ p.2 / p.1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ = (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)<VAR>e_7✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : NormedField.toNormedSpace = NormedAlgebra.toNormedSpace'<GOAL>(p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.2 * (p.1 ^ p.2 * p.1⁻¹)) • ContinuousLinearMap.fst ℝ ℝ ℝ = (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ + (p.1 ^ p.2 * p.2 * p.1⁻¹) • ContinuousLinearMap.fst ℝ ℝ ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.abs ((o.kahler x) y) = ‖x‖ * ‖y‖
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>Complex.normSq ((o.kahler x) y) = (‖x‖ * ‖y‖) ^ 2
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>0 ≤ Complex.abs ((o.kahler x) y)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>0 ≤ ‖x‖ * ‖y‖
<VAR>α : Type u<VAR>a : α<VAR>inst✝¹ : Group α<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>x✝ : Fintype G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : Fintype.card G = p<VAR>g g' : G<VAR>hg : g ≠ 1<GOAL>g' ∈ Submonoid.powers g
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : ContinuousNeg β<VAR>l : Filter α<VAR>f : α → β<VAR>hf : l.ZeroAtFilter f<GOAL>l.ZeroAtFilter (-f)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.reverse ~r (l.rotate n).reverse
<VAR>n : ℤ<GOAL>|↑n.negOnePow| = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<GOAL>↑(toGL 1) = ↑1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<GOAL>LinearMap.id = ↑1
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : Zero α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>h : 1 < b<GOAL>a < a * b
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (f '' K)<VAR>hB₂ : ∀ (U : Set β), qb U → MeasurableSet U<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < (map f μ) U<GOAL>∃ K ⊆ U, pb K ∧ r < (map f μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (f '' K)<VAR>hB₂ : ∀ (U : Set β), qb U → MeasurableSet U<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (f ⁻¹' U)<GOAL>∃ K ⊆ U, pb K ∧ r < (map f μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (f '' K)<VAR>hB₂ : ∀ (U : Set β), qb U → MeasurableSet U<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (f ⁻¹' U)<VAR>K : Set α<VAR>hKU : K ⊆ f ⁻¹' U<VAR>hKc : pa K<VAR>hK : r < μ K<GOAL>∃ K ⊆ U, pb K ∧ r < (map f μ) K
<VAR>α✝ : Type u_1<VAR>m : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>p q : Set α✝ → Prop<VAR>U✝ : Set α✝<VAR>ε : ℝ≥0∞<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ : Measure α<VAR>pa qa : Set α → Prop<VAR>H : μ.InnerRegularWRT pa qa<VAR>f : α → β<VAR>hf : AEMeasurable f μ<VAR>pb qb : Set β → Prop<VAR>hAB : ∀ (U : Set β), qb U → qa (f ⁻¹' U)<VAR>hAB' : ∀ (K : Set α), pa K → pb (f '' K)<VAR>hB₂ : ∀ (U : Set β), qb U → MeasurableSet U<VAR>U : Set β<VAR>hU : qb U<VAR>r : ℝ≥0∞<VAR>hr : r < μ (f ⁻¹' U)<VAR>K : Set α<VAR>hKU : K ⊆ f ⁻¹' U<VAR>hKc : pa K<VAR>hK : r < μ K<GOAL>r < (map f μ) (f '' K)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent✝ : Path α<VAR>v✝ : α<VAR>r✝ x✝ : RBNode α<GOAL>RBNode.Ordered cmp ((left c✝ parent✝ v✝ r✝).fill x✝) ↔ Ordered cmp (left c✝ parent✝ v✝ r✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (left c✝ parent✝ v✝ r✝)) x✝
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>parent✝ : Path α<VAR>v✝ : α<VAR>r✝ x✝ : RBNode α<GOAL>Ordered cmp parent✝ ∧ (All (fun x => cmpLT cmp x v✝) x✝ ∧ All (fun x => cmpLT cmp v✝ x) r✝ ∧ RBNode.Ordered cmp x✝ ∧ RBNode.Ordered cmp r✝) ∧ RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) x✝ ∧ All (RootOrdered cmp parent✝) r✝ ↔ (Ordered cmp parent✝ ∧ All (fun x => cmpLT cmp v✝ x) r✝ ∧ RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) r✝ ∧ RBNode.Ordered cmp r✝) ∧ RBNode.Ordered cmp x✝ ∧ All (fun x => cmpLT cmp x v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>l✝ : RBNode α<VAR>v✝ : α<VAR>parent✝ : Path α<VAR>x✝ : RBNode α<GOAL>RBNode.Ordered cmp ((right c✝ l✝ v✝ parent✝).fill x✝) ↔ Ordered cmp (right c✝ l✝ v✝ parent✝) ∧ RBNode.Ordered cmp x✝ ∧ All (RootOrdered cmp (right c✝ l✝ v✝ parent✝)) x✝
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>c✝ : RBColor<VAR>l✝ : RBNode α<VAR>v✝ : α<VAR>parent✝ : Path α<VAR>x✝ : RBNode α<GOAL>Ordered cmp parent✝ ∧ (All (fun x => cmpLT cmp x v✝) l✝ ∧ All (fun x => cmpLT cmp v✝ x) x✝ ∧ RBNode.Ordered cmp l✝ ∧ RBNode.Ordered cmp x✝) ∧ RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ All (RootOrdered cmp parent✝) x✝ ↔ (Ordered cmp parent✝ ∧ All (fun x => cmpLT cmp x v✝) l✝ ∧ RootOrdered cmp parent✝ v✝ ∧ All (RootOrdered cmp parent✝) l✝ ∧ RBNode.Ordered cmp l✝) ∧ RBNode.Ordered cmp x✝ ∧ All (cmpLT cmp v✝) x✝ ∧ All (RootOrdered cmp parent✝) x✝
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>n : ℕ<GOAL>Continuous fun a => a ^ Int.ofNat n
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s : Set α<VAR>x : α<VAR>n : ℕ<GOAL>Continuous fun a => a ^ Int.negSucc n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : α → β<VAR>ι : Sort u_2<VAR>T : TopologicalSpace α<VAR>f : β → α<VAR>a : β<VAR>s : Set β<GOAL>s ∈ 𝓝 a ↔ s ∈ comap f (𝓝 (f a))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>⟪x, 0⟫_𝕜 = 0
<VAR>n : ℕ<VAR>i j : Fin n.succ<VAR>h : j < i<GOAL>i.cycleRange j = j + 1
<VAR>a✝¹ a✝ : ℕ<GOAL>↑a✝¹ + ↑a✝ = 3 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 3 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 3 ∧ ↑a✝ = 0
<VAR>M : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing M<VAR>a : M<VAR>ha : a ∈ center M<VAR>x✝ : M<GOAL>-a * x✝ = x✝ * -a
<VAR>M : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing M<VAR>a : M<VAR>ha : a ∈ center M<VAR>x✝¹ x✝ : M<GOAL>-a * (x✝¹ * x✝) = -a * x✝¹ * x✝
<VAR>M : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing M<VAR>a : M<VAR>ha : a ∈ center M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * -a * x✝ = x✝¹ * (-a * x✝)
<VAR>M : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing M<VAR>a : M<VAR>ha : a ∈ center M<VAR>x✝¹ x✝ : M<GOAL>x✝¹ * x✝ * -a = x✝¹ * (x✝ * -a)
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<GOAL>(ofNatCode (n + 4)).encodeCode = n + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<GOAL>(ofNatCode (n + 4)).encodeCode = n + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>_m1 : (unpair m).1 < n + 4<GOAL>(ofNatCode (n + 4)).encodeCode = n + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>_m1 : (unpair m).1 < n + 4<VAR>_m2 : (unpair m).2 < n + 4<GOAL>(ofNatCode (n + 4)).encodeCode = n + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>_m1 : (unpair m).1 < n + 4<VAR>_m2 : (unpair m).2 < n + 4<VAR>IH : (ofNatCode m).encodeCode = m<VAR>IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1<VAR>IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2<GOAL>(ofNatCode (n + 4)).encodeCode = n + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>_m1 : (unpair m).1 < n + 4<VAR>_m2 : (unpair m).2 < n + 4<VAR>IH : (ofNatCode m).encodeCode = m<VAR>IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1<VAR>IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2<GOAL>(ofNatCode (n + 4)).encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
<VAR>n : ℕ<VAR>m : ℕ := n.div2.div2<VAR>hm : m < n + 4<VAR>_m1 : (unpair m).1 < n + 4<VAR>_m2 : (unpair m).2 < n + 4<VAR>IH : (ofNatCode m).encodeCode = m<VAR>IH1 : (ofNatCode (unpair m).1).encodeCode = (unpair m).1<VAR>IH2 : (ofNatCode (unpair m).2).encodeCode = (unpair m).2<GOAL>(match n.bodd, n.div2.bodd with | false, false => (ofNatCode (unpair n.div2.div2).1).pair (ofNatCode (unpair n.div2.div2).2) | false, true => (ofNatCode (unpair n.div2.div2).1).comp (ofNatCode (unpair n.div2.div2).2) | true, false => (ofNatCode (unpair n.div2.div2).1).prec (ofNatCode (unpair n.div2.div2).2) | true, true => (ofNatCode n.div2.div2).rfind').encodeCode = bit n.bodd (bit n.div2.bodd n.div2.div2) + 4
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<VAR>ε0 : ↑ε / 2 ≠ 0<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<VAR>ε0 : ↑ε / 2 ≠ 0<VAR>this : infEdist x s < infEdist x s + ↑ε / 2<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<VAR>ε0 : ↑ε / 2 ≠ 0<VAR>this : infEdist x s < infEdist x s + ↑ε / 2<VAR>y : α<VAR>ys : y ∈ s<VAR>dxy : edist x y < infEdist x s + ↑ε / 2<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<VAR>ε0 : ↑ε / 2 ≠ 0<VAR>this✝ : infEdist x s < infEdist x s + ↑ε / 2<VAR>y : α<VAR>ys : y ∈ s<VAR>dxy : edist x y < infEdist x s + ↑ε / 2<VAR>this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y✝ : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>h : infEdist x s + hausdorffEdist s t < ⊤<VAR>ε0 : ↑ε / 2 ≠ 0<VAR>this✝ : infEdist x s < infEdist x s + ↑ε / 2<VAR>y : α<VAR>ys : y ∈ s<VAR>dxy : edist x y < infEdist x s + ↑ε / 2<VAR>this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2<VAR>z : α<VAR>zt : z ∈ t<VAR>dyz : edist y z < hausdorffEdist s t + ↑ε / 2<GOAL>infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>s : Finset α<VAR>t : Finset β<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : Nonempty β<GOAL>s ×ˢ t = univ ↔ s = univ ∧ t = univ
<VAR>α : Type u<VAR>c d : Cardinal.{u}<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>toNat c = n ↔ c = ↑n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Irreducible (Ideal.map (algebraMap R S) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Irreducible (Ideal.map (algebraMap R S) I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>∃ y, normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>∃ y, Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {y}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Multiset.map (fun f => ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f)) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩)}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>∃ a, (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {a} ∧ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm a) = ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>(normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩} ∧ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩) = ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>(normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>Multiset.map (fun a => ↑a) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach = Multiset.map (fun a => ↑a) {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩}
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>x : S<VAR>I : Ideal R<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsIntegrallyClosed R<VAR>inst✝¹ : IsDedekindDomain S<VAR>inst✝ : NoZeroSMulDivisors R S<VAR>hI : I.IsMaximal<VAR>hI' : I ≠ ⊥<VAR>hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤<VAR>hx' : _root_.IsIntegral R x<VAR>hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<VAR>mem_norm_factors : normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))<GOAL>normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) = {normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>h : IsPrimePow n<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n p : R<VAR>k : ℕ<VAR>h : IsPrimePow 0<GOAL>∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<VAR>pp : ¬Nat.Prime p<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<VAR>pp : Nat.Prime p<GOAL>∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n : ℕ<VAR>h : IsPrimePow n<VAR>hn0 : n ≠ 0<VAR>p k : ℕ<VAR>hk0 : 0 < k<VAR>h1 : n.factorization = Finsupp.single p k<VAR>pp : Nat.Prime p<GOAL>n / p ^ n.factorization p = 1