ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B✝ : Matrix n n α<VAR>B : Matrix m n α<VAR>h : IsUnit A.det<GOAL>B * A * A⁻¹ = B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableRel G.Adj<VAR>a₁ a₂ : α<VAR>b : β<VAR>x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>(Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableRel G.Adj<VAR>a₁ a₂ : α<VAR>b : β<VAR>x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableRel G.Adj<VAR>a₁ a₂ : α<VAR>b : β<VAR>x z y : α<VAR>h : G.Adj x y<VAR>w : G.Walk y z<GOAL>G.Adj (x, b).1 ((G.boxProdLeft H b).toHom y).1 ∧ (x, b).2 = ((G.boxProdLeft H b).toHom y).2
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>p a a₁ a₂ b b₁ b₂ c : α<VAR>n✝ : ℕ<VAR>z : ℤ<VAR>x✝¹ : a ≡ b [PMOD p]<VAR>x✝ : b ≡ c [PMOD p]<VAR>m : ℤ<VAR>hm : b - a = m • p<VAR>n : ℤ<VAR>hn : c - b = n • p<GOAL>c - a = (m + n) • p
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<GOAL>map π μ ≪ map π (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<GOAL>map π μ ≪ map π (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<GOAL>∀ ⦃s : Set (G ⧸ Γ)⦄, MeasurableSet s → (map π (μ.restrict 𝓕)) s = 0 → (map π μ) s = 0
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<VAR>s : Set (G ⧸ Γ)<VAR>s_meas : MeasurableSet s<VAR>hs : (map π (μ.restrict 𝓕)) s = 0<GOAL>(map π μ) s = 0
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<VAR>s : Set (G ⧸ Γ)<VAR>s_meas : MeasurableSet s<VAR>hs : (μ.restrict 𝓕) (π ⁻¹' s) = 0<GOAL>μ (π ⁻¹' s) = 0
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<VAR>s : Set (G ⧸ Γ)<VAR>s_meas : MeasurableSet s<VAR>hs : μ (π ⁻¹' s ∩ 𝓕) = 0<GOAL>μ (π ⁻¹' s) = 0
<VAR>G : Type u_1<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝³ : Countable ↥Γ<VAR>inst✝² : MeasurableSpace (G ⧸ Γ)<VAR>inst✝¹ : BorelSpace (G ⧸ Γ)<VAR>inst✝ : μ.IsMulRightInvariant<VAR>π : G → G ⧸ Γ := QuotientGroup.mk<VAR>meas_π : Measurable π<VAR>s : Set (G ⧸ Γ)<VAR>s_meas : MeasurableSet s<VAR>hs : (μ.restrict 𝓕) (π ⁻¹' s) = 0<GOAL>MeasurableSet (π ⁻¹' s)
<VAR>r : ℝ<GOAL>1 < r.toNNReal ↔ 1 < r
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>p : α → Bool<VAR>h : ¬p a = true<GOAL>eraseP p (a :: l) = a :: eraseP p l
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : IsUniform X s ℙ μ<VAR>t : Set E := toMeasurable μ s<GOAL>HasPDF X ℙ μ
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : IsUniform X s ℙ μ<VAR>t : Set E := toMeasurable μ s<GOAL>Measure.map X ℙ = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s t : Seq α<GOAL>map f (s.append t) = (map f s).append (map f t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β<VAR>s t : Seq α<GOAL>IsBisimulation fun s1 s2 => ∃ s t, s1 = map f (s.append t) ∧ s2 = (map f s).append (map f t)
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<GOAL>Irreducible ϖ
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<GOAL>Irreducible ϖ
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = a * b<GOAL>IsUnit a ∨ IsUnit b
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h✝ : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = a * b<VAR>h : ¬IsUnit a ∧ ¬IsUnit b<GOAL>False
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = a * b<VAR>ha : a ∈ maximalIdeal R<VAR>hb : b ∈ maximalIdeal R<GOAL>False
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = a * b<VAR>ha : ∃ a_1, a_1 * ϖ = a<VAR>hb : ∃ a, a * ϖ = b<GOAL>False
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = ϖ * (ϖ * (a * b))<GOAL>ϖ = 0
<VAR>R✝ : Type u<VAR>inst✝⁵ : CommRing R✝<VAR>inst✝⁴ : IsDomain R✝<VAR>inst✝³ : DiscreteValuationRing R✝<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>ϖ : R<VAR>hϖ : ϖ ≠ 0<VAR>h : maximalIdeal R = span {ϖ}<VAR>h2 : ¬IsUnit ϖ<VAR>a b : R<VAR>hab : ϖ = ϖ * (ϖ * (a * b))<GOAL>ϖ * (a * b) ≠ 1
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>h : s ≤ t<GOAL>s.prod ∣ t.prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s : Multiset α<VAR>a : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>z : Multiset α<VAR>h : s ≤ s + z<GOAL>s.prod ∣ (s + z).prod
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<VAR>r : R<GOAL>(ι (Q' Q)) (m, r) = (v Q) m + r • e0 Q
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>𝟙 (J.plusObj (J.plusObj P) ⋙ F) ≫ (J.plusCompIso F (J.plusObj P)).hom ≫ (𝟙 (J.plusObj (J.plusObj P ⋙ F)) ≫ J.plusMap (J.plusCompIso F P).hom) ≫ 𝟙 (J.plusObj (J.plusObj (P ⋙ F))) = (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>𝟙 (J.plusObj (J.plusObj P) ⋙ F) ≫ (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom = (J.plusCompIso F (J.plusObj P)).hom ≫ J.plusMap (J.plusCompIso F P).hom
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b : R<GOAL>RingQuot.add r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a + b) }
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r : R → R → Prop<VAR>a b : R<GOAL>(match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x x_1 => x + x_1) ⋯ ⋯ a b }) = { toQuot := Quot.mk (Rel r) (a + b) }
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : W.CoordinateRing<GOAL>∃ p q, p • 1 + q • (mk W) Y = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : W.CoordinateRing<VAR>h : ∑ i : Fin 2, (CoordinateRing.basis W).equivFun x i • (CoordinateRing.basis W) i = x<GOAL>∃ p q, p • 1 + q • (mk W) Y = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>x : W.CoordinateRing<VAR>h : (CoordinateRing.basis W).equivFun x 0 • 1 + (CoordinateRing.basis W).equivFun x (Fin.succ 0) • (mk W) Y = x<GOAL>∃ p q, p • 1 + q • (mk W) Y = x
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z : K<VAR>n : ℤ<GOAL>im ↑n = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq (Option α)<VAR>s : Finset α<GOAL>eraseNone (image some s) = s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>ContDiffAt 𝕜 (↑(n + 1)) f x ↔ ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>(∃ u ∈ 𝓝[insert x univ] x, ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x) ↔ ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>(∃ u ∈ 𝓝 x, ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x) ↔ ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝²⁰ : SeminormedAddCommGroup E<VAR>inst✝¹⁹ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁸ : SeminormedAddCommGroup F<VAR>inst✝¹⁷ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup G<VAR>inst✝¹⁵ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹² : NontriviallyNormedField 𝕜₃<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>inst✝¹⁰ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁹ : NormedSpace 𝕜₂ F<VAR>inst✝⁸ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁷ : NormedSpace 𝕜₃ G<VAR>inst✝⁶ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁴ : FunLike 𝓕 E F<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E →L[ℝ] F<VAR>C : ℝ≥0<VAR>hf : ∀ (x : E), ‖x‖₊ = 1 → ‖f x‖₊ ≤ C<VAR>x : E<VAR>hx : ‖x‖ = 1<GOAL>‖x‖₊ = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : PerfectField K<VAR>p : K[X]<VAR>h : Irreducible p<VAR>q : K[X]<VAR>sqf : Squarefree (p * q)<VAR>dvd : p ∣ derivative (p * q)<GOAL>False
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : PerfectField K<VAR>p : K[X]<VAR>h : Irreducible p<VAR>q : K[X]<VAR>sqf : Squarefree (p * q)<VAR>dvd : p ∣ q<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>h : minpoly A x = 1<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Ring B'<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra A B'<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>h : minpoly A x = 1<GOAL>1 = 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{u_2, u_1} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : F.IsEquivalence<VAR>inst✝ : (F ⋙ G).IsEquivalence<GOAL>G.IsEquivalence
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{u_2, u_1} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : F.IsEquivalence<VAR>inst✝ : (F ⋙ G).IsEquivalence<GOAL>((F.asEquivalence.inverse ⋙ F.asEquivalence.functor) ⋙ G).IsEquivalence
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α✝ → ℝ≥0∞<VAR>α : Type u_4<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>x✝ : α<VAR>h : x✝ ≠ a<GOAL>⨆ (_ : a = x✝), f x✝ = 0
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : DivisionRing L<VAR>inst✝¹ : DivisionRing M<VAR>S : Type u_1<VAR>inst✝ : SetLike S K<VAR>h : SubfieldClass S K<VAR>x : K<VAR>s : S<VAR>q : ℚ<VAR>hx : x ∈ s<GOAL>q • x ∈ s
<VAR>ε : Type u_1<VAR>p : ε → Prop<VAR>inst✝ : DecidablePred p<VAR>ep ep' : Perm { a // p a }<VAR>en en' : Perm { a // ¬p a }<VAR>a : ε<VAR>h : ¬p a<GOAL>(ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)
<VAR>f g : MulRingNorm ℚ<VAR>h : ∀ (n : ℕ), f ↑n = g ↑n<VAR>z : ℤ<GOAL>f ↑z = g ↑z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<GOAL>∃ K ⊆ s, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>h0 : p ∅<GOAL>∃ K ⊆ s, p K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<GOAL>∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<VAR>U : Set α<VAR>hsU : U ⊇ s<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ s) < ε<GOAL>∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<VAR>U : Set α<VAR>hsU : U ⊇ s<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ s) < ε<VAR>U' : Set α<VAR>hsU' : U' ⊇ U \ s<VAR>hU'o : IsOpen U'<VAR>hμU' : μ U' < ε<GOAL>∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<VAR>U : Set α<VAR>hsU : U ⊇ s<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ s) < ε<VAR>U' : Set α<VAR>hU'o : IsOpen U'<VAR>hμU' : μ U' < ε<VAR>hsU' : U \ U' ⊆ s<GOAL>∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<VAR>U : Set α<VAR>hsU : U ⊇ s<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ s) < ε<VAR>U' : Set α<VAR>hU'o : IsOpen U'<VAR>hμU' : μ U' < ε<VAR>hsU' : U \ U' ⊆ s<VAR>K : Set α<VAR>hKU : K ⊆ U<VAR>hKc : p K<VAR>hKr : μ U < μ K + ε<GOAL>∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ s✝ : Set α<VAR>ε✝ r : ℝ≥0∞<VAR>inst✝ : μ.OuterRegular<VAR>H : μ.InnerRegularWRT p IsOpen<VAR>hd : ∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>h0 : p ∅<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>hεs : ε + ε ≤ μ s<VAR>hr : μ s - (ε + ε) < μ s<VAR>U : Set α<VAR>hsU : U ⊇ s<VAR>hUo : IsOpen U<VAR>hUt : μ U < ⊤<VAR>hμU : μ (U \ s) < ε<VAR>U' : Set α<VAR>hU'o : IsOpen U'<VAR>hμU' : μ U' < ε<VAR>hsU' : U \ U' ⊆ s<VAR>K : Set α<VAR>hKU : K ⊆ U<VAR>hKc : p K<VAR>hKr : μ U < μ K + ε<GOAL>μ s < μ (K \ U') + (ε + ε)
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>M : ModuleCat R<VAR>inst✝ : Subsingleton ↑M<VAR>X : ModuleCat R<VAR>f : M ⟶ X<VAR>x : ↑M<GOAL>f x = default x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>M : ModuleCat R<VAR>inst✝ : Subsingleton ↑M<VAR>X : ModuleCat R<VAR>f : M ⟶ X<VAR>x : ↑M<GOAL>f 0 = default 0
<VAR>X✝ : Type u<VAR>Y✝ : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>p : X × Y → Prop<GOAL>(∀ᶠ (q : X × Y) in 𝓝ˢ (s ×ˢ t), p q) ↔ ∀ x ∈ s, ∀ y ∈ t, ∃ px, (∀ᶠ (x' : X) in 𝓝 x, px x') ∧ ∃ py, (∀ᶠ (y' : Y) in 𝓝 y, py y') ∧ ∀ {x : X}, px x → ∀ {y : Y}, py y → p (x, y)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : Ring α<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<GOAL>-a • t = -(a • t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace Ω<VAR>inst✝⁴ : StandardBorelSpace Ω<VAR>inst✝³ : Nonempty Ω<VAR>ρ : Measure (β × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>E : Type u_4<VAR>f : β × Ω → E<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>hf : IntegrableOn f (Set.univ ×ˢ t) ρ<GOAL>∫ (b : β), ∫ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫ (x : β × Ω) in Set.univ ×ˢ t, f x ∂ρ