ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<GOAL>∃ y, dist x y ≤ δ ∧ dist y z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x y ≤ δ ∧ dist y z < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<VAR>h : dist x z < ε + δ<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : NormedSpace ℝ E<VAR>x y✝ z : E<VAR>δ ε : ℝ<VAR>hδ : 0 ≤ δ<VAR>hε : 0 < ε<VAR>h : dist x z / (ε + δ) < 1<VAR>y : E<VAR>hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z<GOAL>dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<VAR>hf : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>fderivWithin 𝕜 (fun y => f y + c) s x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<VAR>hf : ¬DifferentiableWithinAt 𝕜 f s x<GOAL>¬DifferentiableWithinAt 𝕜 (fun y => f y + c) s x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a b : α<VAR>m : ℕ<VAR>ha : (fun b => some a = b) ((↑s).get m)<VAR>n : ℕ<VAR>hb : (fun b_1 => some b = b_1) ((↑s).get n)<GOAL>a = b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P✝ : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝⁴ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝³ : Module R P✝<VAR>P : Type u_10<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : OrderedAddCommMonoid P<VAR>inst✝ : Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(∀ (x : (i : ι) → Mᵢ i), 0 ≤ (pi Q) x) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P✝ : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁶ : AddCommMonoid P✝<VAR>inst✝⁵ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝⁴ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝³ : Module R P✝<VAR>P : Type u_10<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : OrderedAddCommMonoid P<VAR>inst✝ : Module R P<VAR>Q : (i : ι) → QuadraticMap R (Mᵢ i) P<GOAL>(∀ (x : (i : ι) → Mᵢ i), 0 ≤ ∑ x_1 : ι, (Q x_1) (x x_1)) ↔ ∀ (i : ι) (x : Mᵢ i), 0 ≤ (Q i) x
<VAR>M : Type u_1<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : Pow M ℕ<VAR>inst✝ : NatPowAssoc M<VAR>x : M<VAR>m n : ℕ<GOAL>x ^ (m * n) = (x ^ n) ^ m
<VAR>M : Type u_1<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : Pow M ℕ<VAR>inst✝ : NatPowAssoc M<VAR>x : M<VAR>m n : ℕ<GOAL>x ^ (n * m) = (x ^ n) ^ m
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>s : Set α<VAR>a✝ b : α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>a ⊓ ⨆ i, ⨆ j, f i j = ⨆ i, ⨆ j, a ⊓ f i j
<VAR>R : Type u_1<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : CommRing R<VAR>N : Ideal R<VAR>inst✝ : TopologicalRing R<VAR>s : Set R<VAR>s_op : IsOpen s<GOAL>IsOpen (⇑(mk N) ⁻¹' (⇑(mk N) '' s))
<VAR>R : Type u_1<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : CommRing R<VAR>N : Ideal R<VAR>inst✝ : TopologicalRing R<VAR>s : Set R<VAR>s_op : IsOpen s<GOAL>IsOpen (⋃ x, (fun y => ↑x + y) '' s)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<VAR>d : ℝ<VAR>hd : 0 ≤ d<GOAL>μH[d] s ≤ 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>hs : ∅.Subsingleton<GOAL>μH[d] ∅ ≤ 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<VAR>hs : s.Subsingleton<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>x : X<VAR>hx : x ∈ s<GOAL>μH[d] s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>m : β → γ<VAR>hg : Monotone g<VAR>this : Monotone (map m ∘ g)<VAR>s : Set γ<GOAL>s ∈ map m (f.lift g) ↔ s ∈ f.lift (map m ∘ g)
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, ‖F' x t‖ ≤ bound t<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ∀ x ∈ ball x₀ ε, HasFDerivAt (fun x => F x t) (F' x t) x<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' x₀ t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : H → ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable (F' x₀) (μ.restrict (Ι a b))<VAR>h_bound : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, ‖F' x_1 x‖ ≤ bound x<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ∀ x_1 ∈ ball x₀ ε, HasFDerivAt (fun x_2 => F x_2 x) (F' x_1 x) x_1<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' x₀ t ∂μ) x₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : IsBigOWith c l f g<GOAL>IsBigOWith (Nat.casesOn 0 ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ 0) fun x => g x ^ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f✝ : α → E<VAR>g✝ : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f : α → R<VAR>g : α → 𝕜<VAR>h : IsBigOWith c l f g<VAR>n : ℕ<GOAL>IsBigOWith (Nat.casesOn (n + 2) ‖1‖ fun n => c ^ (n + 1)) l (fun x => f x ^ (n + 2)) fun x => g x ^ (n + 2)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>p : ℝ≥0∞<VAR>G : Type u_5<VAR>F' : Type u_6<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedAddCommGroup F'<VAR>inst✝ : NormedSpace ℝ F'<VAR>m✝ : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>y : F<GOAL>integral μ (const α y) = (μ Set.univ).toReal • y
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d : D<GOAL>𝟙 d ∈ (map φ hφ S).arrows d d
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>𝟙 (φ.obj c) ∈ (map φ hφ S).arrows (φ.obj c) (φ.obj c)
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (𝟙 (φ.obj c))
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>Map.Arrows φ hφ S (φ.obj c) (φ.obj c) (φ.map (𝟙 c))
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<GOAL>𝟙 c ∈ S.arrows c c
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d d' : D<VAR>g : d ⟶ d'<VAR>δ : d ⟶ d<VAR>hδ : δ ∈ (map φ hφ S).arrows d d<GOAL>Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d d' : D<VAR>g : d ⟶ d'<VAR>δ : d ⟶ d<VAR>hδ : ∃ a b g, ∃ (ha : φ.obj a = d) (hb : φ.obj b = d) (_ : g ∈ S.arrows a b), δ = eqToHom ⋯ ≫ φ.map g ≫ eqToHom hb<GOAL>Groupoid.inv g ≫ δ ≫ g ∈ (map φ hφ S).arrows d' d'
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d' : D<VAR>c : C<VAR>g : φ.obj c ⟶ d'<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<GOAL>Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d' : D<VAR>c : C<VAR>g : φ.obj c ⟶ d'<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>this : d' ∈ (im φ hφ).objs<GOAL>Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>d' : D<VAR>c : C<VAR>g : φ.obj c ⟶ d'<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>this : ∃ c, φ.obj c = d'<GOAL>Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows d' d'
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>g : φ.obj c ⟶ φ.obj c'<VAR>this : g ∈ (im φ hφ).arrows (φ.obj c) (φ.obj c')<GOAL>Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>g : φ.obj c ⟶ φ.obj c'<VAR>this : ∃ a b g_1, ∃ (ha : φ.obj a = φ.obj c) (hb : φ.obj b = φ.obj c'), g = eqToHom ⋯ ≫ φ.map g_1 ≫ eqToHom hb<GOAL>Groupoid.inv g ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ g ∈ (map φ hφ S).arrows (φ.obj c') (φ.obj c')
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>hb : φ.obj c = φ.obj c<VAR>hb' : φ.obj c' = φ.obj c'<VAR>f : c ⟶ c'<GOAL>Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (Groupoid.inv (eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb') ≫ (eqToHom ⋯ ≫ φ.map γ ≫ eqToHom cd') ≫ eqToHom ⋯ ≫ φ.map f ≫ eqToHom hb')
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>hb : φ.obj c = φ.obj c<VAR>hb' : φ.obj c' = φ.obj c'<VAR>f : c ⟶ c'<GOAL>Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (inv (φ.map f) ≫ φ.map γ ≫ φ.map f)
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>hb : φ.obj c = φ.obj c<VAR>hb' : φ.obj c' = φ.obj c'<VAR>f : c ⟶ c'<GOAL>Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map (Groupoid.inv f ≫ γ ≫ f))
<VAR>C : Type u<VAR>inst✝¹ : Groupoid C<VAR>S : Subgroupoid C<VAR>D : Type u_1<VAR>inst✝ : Groupoid D<VAR>φ : C ⥤ D<VAR>hφ : Function.Injective φ.obj<VAR>hφ' : im φ hφ = ⊤<VAR>Sn : S.IsNormal<VAR>c : C<VAR>γ : c ⟶ c<VAR>γS : γ ∈ S.arrows c c<VAR>cd' : φ.obj c = φ.obj c<VAR>c' : C<VAR>hb : φ.obj c = φ.obj c<VAR>hb' : φ.obj c' = φ.obj c'<VAR>f : c ⟶ c'<GOAL>Groupoid.inv f ≫ γ ≫ f ∈ S.arrows c' c'
<GOAL>↑π ^ (-1 / 2) * ↑π ^ (1 / 2) = 1
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>i j : n<VAR>hij : i ≠ j<GOAL>(A.updateRow i (A i + A j)).det = A.det
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>x x' : (Quotient.out o).α<GOAL>typein (fun x x_1 => x < x_1) x ≤ typein (fun x x_1 => x < x_1) x' ↔ x ≤ x'
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>x x' : (Quotient.out o).α<GOAL>¬x' < x ↔ x ≤ x'
<VAR>α : Type u_1<VAR>p q : ℚ≥0<VAR>h : q ≤ p<GOAL>↑q ≤ ↑p - 0
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>logb b x ≤ y ↔ x ≤ b ^ y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : DecidableEq L<VAR>inst✝¹⁰ : Algebra R K<VAR>inst✝⁹ : IsFractionRing R K<VAR>inst✝⁸ : Algebra K L<VAR>inst✝⁷ : FiniteDimensional K L<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : IsScalarTower R K L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsDedekindDomain R<VAR>K' : Type u_4<VAR>inst✝² : Field K'<VAR>inst✝¹ : Algebra R K'<VAR>inst✝ : IsFractionRing R K'<VAR>I : ↥(Ideal R)⁰<GOAL>(canonicalEquiv R⁰ K K') ↑((mk0 K) I) = ↑((mk0 K') I)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s : Set α<VAR>hf : StrictMonoOn f s<VAR>a b : α<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>f a < f b ↔ a < b
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : 1 ∈ J<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b✝ : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : 1 ∈ J<VAR>a b : α<VAR>h : b ∈ Submodule.span α ↑I<VAR>oe : 1 = a • x + b<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b✝ : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : 1 ∈ J<VAR>a b : α<VAR>h : b ∈ Submodule.span α ↑I<VAR>oe : 1 = a • x + b<VAR>F : y * 1 = y * (a • x + b)<GOAL>y ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b✝ : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : 1 ∈ J<VAR>a b : α<VAR>h : b ∈ Submodule.span α ↑I<VAR>oe : 1 = a • x + b<VAR>F : y * 1 = y * (a • x + b)<GOAL>a * (x * y) + y * b ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b✝ : α<VAR>inst✝ : CommSemiring α<VAR>I✝ I : Ideal α<VAR>H : I.IsMaximal<VAR>x y : α<VAR>hxy : x * y ∈ I<VAR>hx : x ∉ I<VAR>J : Ideal α := Submodule.span α (insert x ↑I)<VAR>IJ : I ≤ J<VAR>xJ : x ∈ J<VAR>left✝ : 1 ∉ I<VAR>oJ : 1 ∈ J<VAR>a b : α<VAR>h : b ∈ Submodule.span α ↑I<VAR>oe : 1 = a • x + b<VAR>F : y * 1 = y * (a • x + b)<GOAL>b ∈ I
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s : Set E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : SMulCommClass ℝ 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : ContinuousSMul 𝕜 E<GOAL>(𝓝 0).HasBasis (fun s => s ∈ 𝓝 0 ∧ Balanced 𝕜 s ∧ Convex ℝ s) id
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s✝ : Set E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : SMulCommClass ℝ 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ Convex ℝ s<GOAL>∃ i', (i' ∈ 𝓝 0 ∧ Balanced 𝕜 i' ∧ Convex ℝ i') ∧ id i' ⊆ id s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>s✝ : Set E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : SMulCommClass ℝ 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 0 ∧ Convex ℝ s<GOAL>(convexHull ℝ) (balancedCore 𝕜 s) ∈ 𝓝 0 ∧ Balanced 𝕜 ((convexHull ℝ) (balancedCore 𝕜 s)) ∧ Convex ℝ ((convexHull ℝ) (balancedCore 𝕜 s))