ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : Fin 3 → R<VAR>u✝ : R<VAR>hu : IsUnit u✝<VAR>u : R<VAR>P : Fin 3 → R<VAR>hP : P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 - (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) = 0<GOAL>(u • P) y ^ 2 + W'.a₁ * (u • P) x * (u • P) y * (u • P) z + W'.a₃ * (u • P) y * (u • P) z ^ 3 - ((u • P) x ^ 3 + W'.a₂ * (u • P) x ^ 2 * (u • P) z ^ 2 + W'.a₄ * (u • P) x * (u • P) z ^ 4 + W'.a₆ * (u • P) z ^ 6) = 0
<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 : Fin 3 → R<VAR>u : R<VAR>hu : IsUnit u<VAR>this : ∀ (u : R) {P : Fin 3 → R}, W'.Equation P → W'.Equation (u • P)<VAR>h : W'.Equation (u • P)<GOAL>P = hu.unit.inv • u • P
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>f : Equiv.Perm α<GOAL>f ∈ closure {σ | σ.IsSwap} ↔ (fixedBy α f)ᶜ.Finite
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : DecidableEq α<VAR>f : Equiv.Perm α<VAR>x : α<GOAL>swap x (f x) ∈ closure fun x => ∃ x_1 y, x_1 ≠ y ∧ x = swap x_1 y
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a b : ℤ<GOAL>legendreSym p (a * b) = legendreSym p a * legendreSym p b
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ✝ : Filtration ι m0<VAR>inst✝¹ : OrderBot ι<VAR>ℱ : Filtration ι m0<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : Ω → E<VAR>hf : StronglyMeasurable f<VAR>hfint : Integrable f μ<GOAL>Martingale (fun x => f) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ✝ : Measure Ω<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ✝ : Filtration ι m0<VAR>inst✝¹ : OrderBot ι<VAR>ℱ : Filtration ι m0<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : Ω → E<VAR>hf : StronglyMeasurable f<VAR>hfint : Integrable f μ<VAR>i j : ι<VAR>x✝ : i ≤ j<GOAL>μ[(fun x => f) j|↑ℱ i] =ᶠ[ae μ] (fun x => f) i
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<VAR>hnX : AEMeasurable nX μ<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<VAR>hnX : AEMeasurable nX μ<VAR>hnY : AEMeasurable nY μ<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<VAR>hnX : AEMeasurable nX μ<VAR>hnY : AEMeasurable nY μ<VAR>hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ<GOAL>Integrable (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<VAR>hnX : AEMeasurable nX μ<VAR>hnY : AEMeasurable nY μ<VAR>hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ<GOAL>HasFiniteIntegral (X * Y) μ
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X✝ Y✝ : Ω → ℝ<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace β<VAR>X Y : Ω → β<VAR>inst✝¹ : NormedDivisionRing β<VAR>inst✝ : BorelSpace β<VAR>hXY : IndepFun X Y μ<VAR>hX : Integrable X μ<VAR>hY : Integrable Y μ<VAR>nX : Ω → ℝ≥0∞ := fun a => ↑‖X a‖₊<VAR>nY : Ω → ℝ≥0∞ := fun a => ↑‖Y a‖₊<VAR>hXY' : IndepFun (fun a => ‖X a‖₊) (fun a => ‖Y a‖₊) μ<VAR>hXY'' : IndepFun nX nY μ<VAR>hnX : AEMeasurable nX μ<VAR>hnY : AEMeasurable nY μ<VAR>hmul : ∫⁻ (a : Ω), nX a * nY a ∂μ = (∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ<GOAL>(∫⁻ (a : Ω), nX a ∂μ) * ∫⁻ (a : Ω), nY a ∂μ < ⊤
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>x : X<GOAL>IsClopen (setOf (S.Rel x))
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>x : X<GOAL>IsClopen (S.proj ⁻¹' {S.proj x})
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>inst✝ : Nonempty γ<VAR>hf : FactorsThrough g f<VAR>x : α<GOAL>g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>inst✝ : Nonempty γ<VAR>h : ∃ e, g = e ∘ f<VAR>x✝¹ x✝ : α<VAR>hf : f x✝¹ = f x✝<GOAL>g x✝¹ = g x✝
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y \ x = (x ⊓ y ⊔ x \ y) ⊓ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(x ⊓ y ⊔ x \ y) ⊓ y \ x = x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x ⊓ y ⊓ y \ x ⊔ x \ y ⊓ y \ x = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<VAR>h : a < b<GOAL>1 / b < 1 / a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y✝ : α<VAR>inst✝¹ : DecidableRel f.SameCycle<VAR>inst✝ : DecidableRel g.SameCycle<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>y : α<VAR>h : f.SameCycle x y<GOAL>(f.cycleOf x) y = f y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>x y✝ : α<VAR>inst✝¹ : DecidableRel f.SameCycle<VAR>inst✝ : DecidableRel g.SameCycle<VAR>hf : f.IsCycle<VAR>hx : f x ≠ x<VAR>y : α<VAR>h : ¬f.SameCycle x y<GOAL>(f.cycleOf x) y = f y
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>IsCompact (GromovHausdorff.candidatesB X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)), f ∈ GromovHausdorff.candidatesB X Y → f x ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝⁵ : MetricSpace X<VAR>inst✝⁴ : CompactSpace X<VAR>inst✝³ : Nonempty X<VAR>inst✝² : MetricSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : Nonempty Y<VAR>f : GromovHausdorff.ProdSpaceFun X Y<VAR>x y z t : X ⊕ Y<GOAL>Equicontinuous fun x => ⇑↑x
<VAR>α β γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) →. ℕ<VAR>df : DiophPFun f<VAR>v : α → ℕ<VAR>x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}<VAR>x : ℕ<VAR>hS : x ::ₒ v ∈ S<VAR>h : ∃ (h : (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).Dom), (f ((x ::ₒ v) ∘ some, (x ::ₒ v) none).1).get h = ((x ::ₒ v) ∘ some, (x ::ₒ v) none).2<GOAL>v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
<VAR>α β γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) →. ℕ<VAR>df : DiophPFun f<VAR>v : α → ℕ<VAR>x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | f.graph (v ∘ some, v none)}}<VAR>x : ℕ<VAR>hS : x ::ₒ v ∈ S<VAR>h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2<GOAL>v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}
<VAR>α β γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) →. ℕ<VAR>df : DiophPFun f<VAR>v : α → ℕ<VAR>x✝ : v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}<VAR>x : f.Dom v<VAR>hS : f.fn v x ::ₒ v ∈ S<GOAL>∃ (h : (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).Dom), (f ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).1).get h = ((f.fn v x ::ₒ v) ∘ some, (f.fn v x ::ₒ v) none).2
<VAR>α β γ : Type u<VAR>S✝ S' : Set (α → ℕ)<VAR>S : Set (Option α → ℕ)<VAR>d : Dioph S<VAR>f : (α → ℕ) →. ℕ<VAR>df : DiophPFun f<VAR>v : α → ℕ<VAR>x✝ : v ∈ {v | ∃ (h : f.Dom v), f.fn v h ::ₒ v ∈ S}<VAR>x : f.Dom v<VAR>hS : f.fn v x ::ₒ v ∈ S<GOAL>∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2
<VAR>a b c : ℤ<VAR>h2 : ∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → c.natAbs ≤ c1.natAbs<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>heq : a ^ 4 + b ^ 4 = c ^ 2<GOAL>∀ (a1 b1 c1 : ℤ), Fermat42 a1 b1 c1 → (-c).natAbs ≤ c1.natAbs
<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ≥0∞<GOAL>a⁻¹.toReal = a.toReal⁻¹
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>a : α<VAR>l : List α<VAR>inst✝ : IsAntisymm α r<VAR>l₁ l₂ : List α<VAR>hp : l₁ <+~ l₂<VAR>hs₁ : Sorted r l₁<VAR>hs₂ : Sorted r l₂<VAR>w✝ : List α<VAR>h : w✝ ~ l₁<VAR>h' : w✝ <+ l₂<GOAL>l₁ <+ l₂
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<GOAL>ContDiffOn 𝕜 ⊤ (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I)) (((↑i).extend I).symm ≫ (↑j).extend I).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<VAR>h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I<GOAL>ContDiffOn 𝕜 ⊤ (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I)) (((↑i).extend I).symm ≫ (↑j).extend I).source
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<VAR>h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I<VAR>x : E<VAR>hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source<GOAL>ContDiffWithinAt 𝕜 ⊤ (fderivWithin 𝕜 (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I)) (((↑i).extend I).symm ≫ (↑j).extend I).source x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<VAR>h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I<VAR>x : E<VAR>hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source<GOAL>ContDiffWithinAt 𝕜 ⊤ (↑((↑j).extend I) ∘ ↑((↑i).extend I).symm) (range ↑I) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>i j : ↑(atlas H M)<VAR>h : (((↑i).extend I).symm ≫ (↑j).extend I).source ⊆ range ↑I<VAR>x : E<VAR>hx : x ∈ (((↑i).extend I).symm ≫ (↑j).extend I).source<GOAL>(((↑i).extend I).symm ≫ (↑j).extend I).source ∈ 𝓝[range ↑I] x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>a / b < c / d ↔ a * d < c * b
<VAR>α✝ α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>h : Commute x y<VAR>n✝ : ℕ<GOAL>∑ i ∈ range (n✝ + 1), x ^ i * y ^ (n✝ + 1 - 1 - i) = ∑ i ∈ range (n✝ + 1), y ^ i * x ^ (n✝ + 1 - 1 - i)
<VAR>α✝ α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>h : Commute x y<VAR>n✝ : ℕ<GOAL>∑ x_1 ∈ range (n✝ + 1), x ^ x_1 * y ^ (n✝ - x_1) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
<VAR>α✝ α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>h : Commute x y<VAR>n✝ : ℕ<GOAL>∑ r ∈ range (n✝ + 1), x ^ (n✝ - r) * y ^ (n✝ - (n✝ - r)) = ∑ x_1 ∈ range (n✝ + 1), y ^ x_1 * x ^ (n✝ - x_1)
<VAR>α✝ α : Type u<VAR>inst✝ : Semiring α<VAR>x y : α<VAR>h : Commute x y<VAR>n✝ i : ℕ<VAR>hi : i ∈ range (n✝ + 1)<GOAL>x ^ (n✝ - i) * y ^ (n✝ - (n✝ - i)) = y ^ i * x ^ (n✝ - i)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>x \ y = x ↔ Disjoint x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>inst✝² : Fintype α<VAR>f : α → β<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : Fintype { a // p a }<GOAL>Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (filter p univ).val
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>h : a ≤ b<VAR>hb : 0 ≤ b<GOAL>b⁻¹ * a ≤ 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex k P n<VAR>h : Set.range s₁.points = Set.range s₂.points<GOAL>centroid k univ s₁.points = centroid k univ s₂.points
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>n : ℕ<VAR>s₁ s₂ : Simplex k P n<VAR>h : s₁.points '' ↑univ = s₂.points '' ↑univ<GOAL>centroid k univ s₁.points = centroid k univ s₂.points
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalRing R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a : A<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a)) _auto✝<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun x => -x) a = -a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>s t : Set β<VAR>κ : Kernel α β<VAR>hs : MeasurableSet s<VAR>a : α<VAR>f : β → ℝ≥0∞<GOAL>∫⁻ (b : β), f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in s, f b ∂κ a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ ⊥.jacobson<VAR>y z : R<VAR>hz : z * y * x + z - 1 ∈ ⊥<GOAL>(x * y + 1) * z = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G H : SimpleGraph α<VAR>n : ℕ<VAR>s : Finset α<VAR>a b c : α<GOAL>G.IsNClique n {a} ↔ n = 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>√(normSq z) = ‖z‖
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<GOAL>(condCount s) u * (condCount (s ∪ t)) s + (condCount t) u * (condCount (s ∪ t)) t = (condCount (s ∪ t)) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>u : Set Ω<VAR>hs ht : ∅.Finite<VAR>hst : Disjoint ∅ ∅<GOAL>(condCount ∅) u * (condCount (∅ ∪ ∅)) ∅ + (condCount ∅) u * (condCount (∅ ∪ ∅)) ∅ = (condCount (∅ ∪ ∅)) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>t u : Set Ω<VAR>ht : t.Finite<VAR>hs : ∅.Finite<VAR>hst : Disjoint ∅ t<VAR>ht' : t.Nonempty<GOAL>(condCount ∅) u * (condCount (∅ ∪ t)) ∅ + (condCount t) u * (condCount (∅ ∪ t)) t = (condCount (∅ ∪ t)) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s u : Set Ω<VAR>hs : s.Finite<VAR>hs' : s.Nonempty<VAR>ht : ∅.Finite<VAR>hst : Disjoint s ∅<GOAL>(condCount s) u * (condCount (s ∪ ∅)) s + (condCount ∅) u * (condCount (s ∪ ∅)) ∅ = (condCount (s ∪ ∅)) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>(condCount s) u * (condCount (s ∪ t)) s + (condCount t) u * (condCount (s ∪ t)) t = (condCount (s ∪ t)) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>(Measure.count s)⁻¹ * Measure.count (s ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ s)) + (Measure.count t)⁻¹ * Measure.count (t ∩ u) * ((Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ t)) = (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Measure.count s * (Measure.count s)⁻¹ * Measure.count (s ∩ u) * (Measure.count (s ∪ t))⁻¹ + Measure.count t * (Measure.count t)⁻¹ * Measure.count (t ∩ u) * (Measure.count (s ∪ t))⁻¹ = (Measure.count (s ∪ t))⁻¹ * Measure.count ((s ∪ t) ∩ u)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Disjoint (s ∩ u) (t ∩ u)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>MeasurableSet (t ∩ u)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Measure.count t ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Measure.count t ≠ ⊤
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Measure.count s ≠ 0
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<VAR>ht : t.Finite<VAR>hst : Disjoint s t<VAR>hs' : s.Nonempty<VAR>ht' : t.Nonempty<GOAL>Measure.count s ≠ ⊤
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : r₁ ≤ 0<VAR>hr₂ : 0 ≤ r₂<GOAL>Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : CompleteSpace 𝕜<VAR>n : ℕ∞<VAR>f : E → F →L[𝕜] G<VAR>s : Set E<VAR>inst✝ : FiniteDimensional 𝕜 F<GOAL>ContDiffOn 𝕜 n f s ↔ ∀ (y : F), ContDiffOn 𝕜 n (fun x => (f x) y) s