ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<GOAL>∀ (x y : V), s(x, y) ∈ (G.replaceVertex s t).edgeSet ↔ s(x, y) ∈ (G.edgeSet \ G.incidenceSet t ∪ (fun x => s(x, t)) '' G.neighborSet s) \ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<GOAL>∀ (x y : V), (if x = t then if y = t then False else G.Adj s y else if y = t then G.Adj x s else G.Adj x y) ↔ (G.Adj x y ∧ ¬(G.Adj x y ∧ (t = x ∨ t = y)) ∨ s(x, y) ∈ (fun x => s(x, t)) '' G.neighborSet s) ∧ s(x, y) ∉ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : x✝ = t<VAR>h✝ : y✝ = t<GOAL>False ↔ (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s) ∧ s(x✝, y✝) ∉ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : x✝ = t<VAR>h✝ : ¬y✝ = t<GOAL>G.Adj s y✝ ↔ (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s) ∧ s(x✝, y✝) ∉ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : ¬x✝ = t<VAR>h✝ : y✝ = t<GOAL>G.Adj x✝ s ↔ (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s) ∧ s(x✝, y✝) ∉ {s(t, t)}
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t : V<VAR>ha : G.Adj s t<VAR>e : Sym2 V<VAR>x✝ y✝ : V<VAR>h✝¹ : ¬x✝ = t<VAR>h✝ : ¬y✝ = t<GOAL>G.Adj x✝ y✝ ↔ (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x => s(x, t)) '' G.neighborSet s) ∧ s(x✝, y✝) ∉ {s(t, t)}
<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>a b : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h : b ≤ a<GOAL>∫ (x : ℝ) in a..b, f x ∂μ = -∫ (x : ℝ) in Ioc b a, f x ∂μ
<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>a : R<VAR>b : S<VAR>b' : R<VAR>hb : (algebraMap R S) b' = b<GOAL>IsInteger R (a • b)
<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>a : R<VAR>b : S<VAR>b' : R<VAR>hb : (algebraMap R S) b' = b<GOAL>(algebraMap R S) (a * b') = a • b
<VAR>m : ℤ<VAR>n : ℕ<GOAL>↑m * powHalf (Submonoid.log (Submonoid.pow 2 n)) = ↑m * powHalf n
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>lift f g H ≫ f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>inv (pullback.snd f g) ≫ pullback.fst f g ≫ f = g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y Z : PresheafedSpace C<VAR>f : X ⟶ Z<VAR>hf : IsOpenImmersion f<VAR>g : Y ⟶ Z<VAR>s : PullbackCone f g<VAR>H : Set.range ⇑g.base ⊆ Set.range ⇑f.base<GOAL>pullback.fst f g ≫ f = pullback.snd f g ≫ g
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.rev.succAbove i = (p.succAbove i.rev).rev
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : i.succ ≤ p.rev<GOAL>p.rev.succAbove i = (p.succAbove i.rev).rev
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>h : p.rev ≤ i.castSucc<GOAL>p.rev.succAbove i = (p.succAbove i.rev).rev
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H✝ K : Subgroup G<VAR>k : Set G<VAR>H H' : Subgroup G<GOAL>H ⊔ H' = closure (↑H ∪ ↑H')
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict t).restrict s = (μ.restrict s).restrict t
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g✝ : ((i : δ) → π i) → ℝ≥0∞<VAR>x y : (i : δ) → π i<VAR>i : δ<VAR>f g : ((i : δ) → π i) → ℝ≥0∞<VAR>hst : s ⊆ t<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ<GOAL>∫⋯∫⁻_t, f ∂μ = ∫⋯∫⁻_t, g ∂μ
<VAR>α : Type u<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : DenselyOrdered α<VAR>inst✝³ : Monoid α<VAR>inst✝² : ExistsMulOfLE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a ≤ b * ε<VAR>x : α<VAR>hxb : b < x<GOAL>a ≤ x
<VAR>α : Type u<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : DenselyOrdered α<VAR>inst✝³ : Monoid α<VAR>inst✝² : ExistsMulOfLE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : ∀ (ε : α), 1 < ε → a ≤ b * ε<VAR>ε : α<VAR>hxb : b < b * ε<GOAL>a ≤ b * ε
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Subsingleton R<GOAL>p.degree = ⊥
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>n : ℤ<VAR>hpn : IsCoprime n ↑p<VAR>this✝ : Fact (Nat.Prime p)<VAR>this : ¬↑n = 0<GOAL>n ^ (p - 1) ≡ 1 [ZMOD ↑p]
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s = 𝓝ˢ t ↔ s = t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>s t : Set X<GOAL>𝓝ˢ s ≤ 𝓝ˢ t ∧ 𝓝ˢ t ≤ 𝓝ˢ s ↔ s ≤ t ∧ t ≤ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LT α<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a * b < b<GOAL>a * b < 1 * b
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivWithinAt I' I'' g u (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hst : s ⊆ f ⁻¹' u<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) s x (g'.comp f')
<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>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivWithinAt I' I'' g u (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hst : s ⊆ f ⁻¹' u<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I'' x (g ∘ f)) (g'.comp f') (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivWithinAt I' I'' g u (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hst : s ⊆ f ⁻¹' u<VAR>A : HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g'.comp f') (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I'' x (g ∘ f)) (g'.comp f') (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>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>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>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>n : ℕ∞<VAR>hg : HasMFDerivWithinAt I' I'' g u (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f s x f'<VAR>hst : s ⊆ f ⁻¹' u<VAR>A : HasFDerivWithinAt (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (g'.comp f') (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<GOAL>writtenInExtChartAt I I'' x (g ∘ f) (↑(extChartAt I x) x) = (writtenInExtChartAt I' I'' (f x) g ∘ writtenInExtChartAt I I' x f) (↑(extChartAt I x) x)
<VAR>K : Type u<VAR>inst✝ : Field K<GOAL>intDegree 0 = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s✝ s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>s : Set ι<GOAL>s.pi t ∩ sᶜ.pi t = univ.pi t
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : MulZeroClass α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : MulPosStrictMono α<VAR>inst✝ : MulPosReflectLT α<VAR>h : 0 < b<GOAL>0 < a * b ↔ 0 < a
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(β_ X (Y ⊗ Z)).hom = (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom = (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y Z : C<GOAL>((α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom) ≫ (α_ Y Z X).hom = ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv) ≫ (α_ Y Z X).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<GOAL>(μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<GOAL>(μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<VAR>this : IsFiniteMeasure (μ.withDensity f)<GOAL>(μ.withDensityᵥ fun x => (f x).toReal) = (μ.withDensity f).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<VAR>this : IsFiniteMeasure (μ.withDensity f)<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ.withDensityᵥ fun x => (f x).toReal) i = ↑(μ.withDensity f).toSignedMeasure i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<VAR>this : IsFiniteMeasure (μ.withDensity f)<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>∀ᵐ (x : α) ∂μ.restrict i, f x < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<VAR>this : IsFiniteMeasure (μ.withDensity f)<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>hfi : Integrable (fun x => (f x).toReal) μ<VAR>this : IsFiniteMeasure (μ.withDensity f)<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>∫⁻ (x : α) in i, f x ∂μ ≤ ∫⁻ (x : α) in Set.univ, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MonoidWithZero α<GOAL>Quot.out 0 = 0
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : LocalRing R<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i = ⊥
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : LocalRing R<VAR>h : I ≠ ⊤<VAR>x✝ : ℕ<GOAL>I ^ x✝ = I ^ x✝ • ⊤
<VAR>R M : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : LocalRing R<VAR>h : I ≠ ⊤<VAR>x✝ : ℕ<VAR>i : R<GOAL>i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤
<VAR>b✝ b : ℂ<VAR>c T : ℝ<GOAL>‖cexp (-b * (↑T + ↑c * I) ^ 2)‖ = rexp (-(b.re * T ^ 2 - 2 * b.im * c * T - b.re * c ^ 2))
<VAR>b✝ b : ℂ<VAR>c T : ℝ<GOAL>rexp (-((↑b.re + ↑b.im * I) * (↑T + ↑c * I) ^ 2).re) = rexp (-((↑b.re + ↑b.im * I).re * T ^ 2 - 2 * (↑b.re + ↑b.im * I).im * c * T - (↑b.re + ↑b.im * I).re * c ^ 2))
<VAR>b✝ b : ℂ<VAR>c T : ℝ<GOAL>rexp (-(b.re * ((T + (c * 0 - 0 * 1)) * (T + (c * 0 - 0 * 1)) - (0 + (c * 1 + 0 * 0)) * (0 + (c * 1 + 0 * 0))) - b.im * ((T + (c * 0 - 0 * 1)) * (0 + (c * 1 + 0 * 0)) + (0 + (c * 1 + 0 * 0)) * (T + (c * 0 - 0 * 1))))) = rexp (-(b.re * (T * T) - 2 * b.im * c * T - b.re * (c * c)))
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>sf 4 * n = (∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)!
<VAR>n✝ : ℕ<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<GOAL>(∏ i ∈ range (2 * n), (2 * i + 1)!) ^ 2 * 2 ^ (2 * n) * (2 * n)! = ((∏ i ∈ range (2 * n), (2 * i + 1)!) * 2 ^ n) ^ 2 * (2 * n)!
<VAR>R : Type u<VAR>inst✝⁶ : Ring R<VAR>Q : Type v<VAR>inst✝⁵ : AddCommGroup Q<VAR>inst✝⁴ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>c : Set (ExtensionOf i f)<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>a : ExtensionOf i f<VAR>a_mem : a ∈ c<VAR>b : ExtensionOf i f<VAR>b_mem : b ∈ c<VAR>neq : (fun x => x.toLinearPMap) a ≠ (fun x => x.toLinearPMap) b<GOAL>(fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) a) ((fun x => x.toLinearPMap) b) ∨ (fun x x_1 => x ≤ x_1) ((fun x => x.toLinearPMap) b) ((fun x => x.toLinearPMap) a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s✝ s : Set α<VAR>t : Set β<GOAL>latticeClosure (s ×ˢ t) = latticeClosure s ×ˢ latticeClosure t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : DistribLattice β<VAR>s✝ s : Set α<VAR>t : Set β<GOAL>supClosure (infClosure (s ×ˢ t)) = supClosure (infClosure s) ×ˢ supClosure (infClosure t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : ∀ (x : α), ↑e x = ↑e' x<VAR>hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x<VAR>hs : e.source = e'.source<VAR>A : ↑e = ↑e'<VAR>B : ↑e.symm = ↑e'.symm<GOAL>e = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : ∀ (x : α), ↑e x = ↑e' x<VAR>hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x<VAR>hs : e.source = e'.source<VAR>A : ↑e = ↑e'<VAR>B : ↑e.symm = ↑e'.symm<VAR>I : ↑e '' e.source = e.target<GOAL>e = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e✝ : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>e e' : PartialEquiv α β<VAR>h : ∀ (x : α), ↑e x = ↑e' x<VAR>hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x<VAR>hs : e.source = e'.source<VAR>A : ↑e = ↑e'<VAR>B : ↑e.symm = ↑e'.symm<VAR>I : ↑e '' e.source = e.target<VAR>I' : ↑e' '' e'.source = e'.target<GOAL>e = e'
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>l m : List α<VAR>a : α<VAR>_H : ∀ (hl : m ≠ []), Chain r ↑m ↔ List.Chain r (m.getLast hl) m<VAR>hl✝ : m ++ [a] ≠ []<GOAL>Chain r ↑(m ++ [a]) ↔ List.Chain r ((m ++ [a]).getLast hl✝) (m ++ [a])
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>‖y‖ / (o.oangle x (x + y)).sin = ‖x + y‖
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>S✝ T✝ : Submodule R M<VAR>h : S✝ ≤ T✝<VAR>S T : Submodule R M<VAR>hST : T ≤ S<GOAL>Nat.card ↥(map T.mkQ S) * Nat.card (M ⧸ S) = Nat.card (M ⧸ T)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>ht : NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<VAR>u : Set α := {x | x ∈ s ∧ f x ≠ 0}<GOAL>IntegrableOn f t μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>ht : NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<VAR>u : Set α := {x | x ∈ s ∧ f x ≠ 0}<VAR>hu : IntegrableOn f u μ<GOAL>IntegrableOn f t μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>ht : NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<VAR>u : Set α := {x | x ∈ s ∧ f x ≠ 0}<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := toMeasurable μ u<VAR>A : IntegrableOn f v μ<VAR>B : IntegrableOn f (t \ v) μ<GOAL>IntegrableOn f t μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>ht : NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<VAR>u : Set α := {x | x ∈ s ∧ f x ≠ 0}<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := toMeasurable μ u<VAR>A : IntegrableOn f v μ<VAR>B : IntegrableOn f (t \ v) μ<GOAL>t ⊆ v ∪ t \ v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>hf : IntegrableOn f s μ<VAR>ht : NullMeasurableSet t μ<VAR>h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0<VAR>u : Set α := {x | x ∈ s ∧ f x ≠ 0}<VAR>hu : IntegrableOn f u μ<VAR>v : Set α := toMeasurable μ u<VAR>A : IntegrableOn f v μ<VAR>B : IntegrableOn f (t \ v) μ<GOAL>t ⊆ v ∪ t
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b