ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>U V : Opens M<VAR>h : U ≤ V<VAR>x : M<VAR>hx : x ∈ U<VAR>y : H<GOAL>ContDiffWithinAt 𝕜 n (↑I ∘ ↑I.symm) (range ↑I) (↑I y)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<GOAL>evalEval 0 0 W.polynomialY = W.a₃
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharP R n<VAR>I : Ideal R<GOAL>CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>n : ℕ<VAR>inst✝ : CharP R n<VAR>I : Ideal R<GOAL>(∀ (x : ℕ), ↑x ∈ I → ↑x = 0) ↔ Ideal.comap (Nat.castRingHom R) I ≤ Ideal.comap (Nat.castRingHom R) ⊥
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<GOAL>P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x) ↔ P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<VAR>h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<GOAL>P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<VAR>h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>this : P ((f ∘ ↑e.symm) ∘ ↑e.symm.symm) (↑e.symm.symm ⁻¹' (↑e.symm ⁻¹' s)) (↑e.symm (↑e x))<GOAL>P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<VAR>h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' (↑e.symm ⁻¹' s)) x<GOAL>P f s x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<VAR>h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' (↑e.symm ⁻¹' s)) x<GOAL>(f ∘ ↑e.symm) ∘ ↑e =ᶠ[𝓝 x] f
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>P : (H → H') → Set H → H → Prop<VAR>s✝ t u : Set H<VAR>x✝ : H<VAR>hG : G.LocalInvariantProp G' P<VAR>s : Set H<VAR>x : H<VAR>f : H → H'<VAR>e : PartialHomeomorph H H<VAR>he : e ∈ G<VAR>hxe : x ∈ e.source<VAR>h : P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)<VAR>this : P ((f ∘ ↑e.symm) ∘ ↑e) (↑e ⁻¹' (↑e.symm ⁻¹' s)) x<GOAL>↑e ⁻¹' (↑e.symm ⁻¹' s) =ᶠ[𝓝 x] s
<VAR>x y : ℂ<GOAL>cexp x = cexp ↑x.re * (cos ↑x.im + sin ↑x.im * I)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))<VAR>hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))<GOAL>∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>hBf : ∃ c < a, ∃ B, f =O[l] fun z => expR (B * expR (c * |u z|))<VAR>hBg : ∃ c < a, ∃ B, g =O[l] fun z => expR (B * expR (c * |u z|))<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<GOAL>∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>∃ c < a, ∃ B, (f - g) =O[l] fun z => expR (B * expR (c * |u z|))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>(f - g) =O[l] fun z => expR (max 0 (max Bf Bg) * expR (max cf cg * |u z|))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>cf ≤ max cf cg
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>0 ≤ max 0 (max Bf Bg)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>Bf ≤ max 0 (max Bf Bg)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>cg ≤ max cf cg
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a : ℝ<VAR>f g : ℂ → E<VAR>l : Filter ℂ<VAR>u : ℂ → ℝ<VAR>this : ∀ {c₁ c₂ B₁ B₂ : ℝ}, c₁ ≤ c₂ → 0 ≤ B₂ → B₁ ≤ B₂ → ∀ (z : ℂ), ‖expR (B₁ * expR (c₁ * |u z|))‖ ≤ ‖expR (B₂ * expR (c₂ * |u z|))‖<VAR>cf : ℝ<VAR>hcf : cf < a<VAR>Bf : ℝ<VAR>hOf : f =O[l] fun z => expR (Bf * expR (cf * |u z|))<VAR>cg : ℝ<VAR>hcg : cg < a<VAR>Bg : ℝ<VAR>hOg : g =O[l] fun z => expR (Bg * expR (cg * |u z|))<GOAL>Bg ≤ max 0 (max Bf Bg)
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>hl : l.Sized<GOAL>(l.rotateR x r).size = l.size + r.size + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝² : CommRing R<VAR>M N : Matrix m m R<VAR>b : m → α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : DecidableEq α<VAR>d : (i : α) → Matrix (m' i) (m' i) R<VAR>i : α<VAR>i' : m' i<VAR>j : α<VAR>j' : m' j<VAR>h : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst<GOAL>blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace β<VAR>inst✝² : MeasurableSpace γ<VAR>inst✝¹ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>inst✝ : SigmaFinite μb<GOAL>SigmaFinite (map f μa)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>h : u ≠ v<VAR>p : G.Walk u v<GOAL>p ∈ {p | p.length = 0} ↔ p ∈ ∅
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>h : u ≠ v<VAR>p : G.Walk u v<GOAL>¬p.length = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p✝ : α → Prop<VAR>inst✝² : DecidablePred p✝<VAR>s : Multiset α<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>l : List α<GOAL>countP p (filter (fun a => ¬q a) (Quot.mk Setoid.r l)) = List.countP (fun x => decide (p x)) (List.filter (fun a => !decide (q a)) l)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>-⁅y, x⁆ = ⁅x, y⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<VAR>h : ⁅x + y, x⁆ + ⁅x + y, y⁆ = 0<GOAL>-⁅y, x⁆ = ⁅x, y⁆
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>I : Ideal R<VAR>h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0<VAR>x : ℕ<GOAL>↑x = 0 ↔ p ∣ x
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>I : Ideal R<VAR>h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0<VAR>x : ℕ<GOAL>(Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>I : Ideal R<VAR>h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0<VAR>x : ℕ<GOAL>↑x - 0 ∈ I ↔ ↑x = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : CharP R p<VAR>I : Ideal R<VAR>h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0<VAR>x : ℕ<GOAL>↑x ∈ I ↔ ↑x = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u✝ v✝ u' v' : V<VAR>p✝ : G.Walk u✝ v✝<VAR>u v : V<VAR>p : G.Walk u v<VAR>H : SimpleGraph V<VAR>w : V<VAR>q : G.Walk v w<VAR>hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet<GOAL>(p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>s : ↥M<GOAL>mk' S x s = 0 ↔ ∃ m, ↑m * x = 0
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<GOAL>HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<GOAL>HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<GOAL>HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<VAR>hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1<GOAL>HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<VAR>hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1<VAR>hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1<GOAL>HasDerivAt Gammaℝ (-(↑γ + log (4 * ↑π)) / 2) 1
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<VAR>hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1<VAR>hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1<GOAL>-log ↑π / 2 / ↑√π * Gamma (1 / 2) + f 1 * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<VAR>hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1<VAR>hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1<GOAL>-log ↑π / 2 / ↑√π * Gamma (1 / 2) + ↑π ^ (-1 / 2) * (-↑√π * (↑γ + 2 * log 2) / 2) = -(↑γ + log (4 * ↑π)) / 2
<VAR>f : ℂ → ℂ := fun s => ↑π ^ (-s / 2)<VAR>g : ℂ → ℂ := fun s => Gamma (s / 2)<VAR>aux : ↑π ^ (1 / 2) = ↑√π<VAR>aux2 : ↑√π ≠ 0<VAR>hf : HasDerivAt f (-log ↑π / 2 / ↑√π) 1<VAR>hg : HasDerivAt g (-↑√π * (↑γ + 2 * log 2) / 2) 1<GOAL>-(↑γ + log ↑(2 ^ 2 * π)) / 2 = -(↑γ + log (4 * ↑π)) / 2
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<GOAL>mkRat n₁ d₁ * mkRat n₂ d₂ = mkRat (n₁ * n₂) (d₁ * d₂)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G₁ G₂ : SimpleGraph V<VAR>H : SimpleGraph W<VAR>f : G →g G'<VAR>hinj : Injective ⇑f<VAR>e₁ : Sym2 V<VAR>h₁ : e₁ ∈ G.edgeSet<VAR>e₂ : Sym2 V<VAR>h₂ : e₂ ∈ G.edgeSet<GOAL>⟨Sym2.map (⇑f) e₁, ⋯⟩ = ⟨Sym2.map (⇑f) e₂, ⋯⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G₁ G₂ : SimpleGraph V<VAR>H : SimpleGraph W<VAR>f : G →g G'<VAR>hinj : Injective ⇑f<VAR>e₁ : Sym2 V<VAR>h₁ : e₁ ∈ G.edgeSet<VAR>e₂ : Sym2 V<VAR>h₂ : e₂ ∈ G.edgeSet<GOAL>Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n✝ n : ℕ<VAR>ih : ⊤ ^ n = ⊤<GOAL>⊤ ^ n.succ = ⊤
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type u_2<VAR>inst✝ : MulAction R X<VAR>p : R<VAR>r : X<VAR>s : ↥S<GOAL>(p /ₒ s) • (r /ₒ 1) = p • r /ₒ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddCommMonoid M<VAR>p✝ p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α →₀ M<VAR>x : α<VAR>hx : x ∈ Finset.filter p f.support<GOAL>single x ((filter p f) x) = single x (f x)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f<VAR>hfi : IntervalIntegrable f μ a b<GOAL>0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f<VAR>hfi : IntervalIntegrable f μ a b<VAR>hab : a < b<GOAL>0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hf : 0 ≤ᶠ[ae (μ.restrict (Ι a b))] f<VAR>hfi : IntervalIntegrable f μ a b<VAR>hba : b ≤ a<GOAL>0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (support f ∩ Ioc a b)
<VAR>S : Set Ordinal.{u}<GOAL>enumOrd S 0 = sInf S
<VAR>S : Set Ordinal.{u}<GOAL>sInf (S ∩ {b | ∀ c < 0, enumOrd S c < b}) = sInf S
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<VAR>s : Set E<GOAL>dimH s ≤ dimH (⇑e '' s)
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j<GOAL>⨅ a, ⨅ a', f a + g a' = iInf f + iInf g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι'✝ : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t✝ : ι✝ → α<VAR>ht✝ : Independent t✝<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : Independent (t ∘ f)<VAR>hf : Surjective f<VAR>i' : ι'<GOAL>Disjoint (t (f i')) (⨆ j, ⨆ (_ : j ≠ f i'), t j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>ι'✝ : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t✝ : ι✝ → α<VAR>ht✝ : Independent t✝<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>t : ι → α<VAR>f : ι' → ι<VAR>ht : Independent (t ∘ f)<VAR>hf : Surjective f<VAR>i' : ι'<GOAL>Disjoint (t (f i')) (⨆ x, ⨆ (_ : f x ≠ f i'), t (f x))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<GOAL>M ∈ Set.range ⇑(scalar n)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : IsEmpty n<GOAL>M ∈ Set.range ⇑(scalar n)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<GOAL>M ∈ Set.range ⇑(scalar n)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<VAR>i : n<GOAL>M ∈ Set.range ⇑(scalar n)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<VAR>i j k : n<GOAL>(scalar n) (M i i) j k = M j k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<VAR>i j k : n<GOAL>diagonal (fun x => M i i) j k = M j k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<VAR>i j : n<GOAL>diagonal (fun x => M i i) j j = M j j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Fintype n<VAR>M : Matrix n n α<VAR>hM : Pairwise fun i j => Commute (stdBasisMatrix i j 1) M<VAR>h✝ : Nonempty n<VAR>i j k : n<VAR>hkl : j ≠ k<GOAL>diagonal (fun x => M i i) j k = M j k
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → F<VAR>hP : W.Equation P<VAR>hQ : W.Equation Q<VAR>hPz : P z ≠ 0<VAR>hQz : Q z ≠ 0<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W.addXYZ P Q = addU P Q • ![1, 1, 0]
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R✝ : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>R : Type u_14<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : DistribMulAction R α<VAR>x : R<VAR>M : o → Matrix m n α<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>blockDiagonal (x • M) i✝ j✝ = (x • blockDiagonal M) i✝ j✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R✝ : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>R : Type u_14<VAR>inst✝² : Monoid R<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : DistribMulAction R α<VAR>x : R<VAR>M : o → Matrix m n α<VAR>i✝ : m × o<VAR>j✝ : n × o<GOAL>(if i✝.2 = j✝.2 then x • M i✝.2 i✝.1 j✝.1 else 0) = x • if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>hq_pos : 0 < q<VAR>h0 : ¬p = 0<VAR>hp_top : ¬p = ⊤<GOAL>eLpNorm (fun x => ‖f x‖ ^ q) p μ = eLpNorm f (p * ENNReal.ofReal q) μ ^ q