ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x n : ℂ<GOAL>(if x = 0 then if n = 0 then 1 else 0 else if x.arg = π then (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else (cexp (log x * n))⁻¹) = if x.arg = π then if x = 0 then if n = 0 then 1 else 0 else (cexp ((starRingEnd ℂ) (log x) * n))⁻¹ else if x = 0 then if n = 0 then 1 else 0 else (cexp (log x * n))⁻¹
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommMonoid N<VAR>inst✝³ : Module R N<VAR>inst✝² : AddCommMonoid P<VAR>inst✝¹ : Module R P<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>l : ↥(supported M R s)<VAR>a : α<VAR>h : a ∉ s<GOAL>↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a
<VAR>S : Type u<VAR>inst✝ : Semiring S<VAR>n : ℕ<VAR>h : n ≠ 0<GOAL>eval 0 (ascPochhammer S n) = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : Limits.IsInitial A<GOAL>A.str ≫ strInv h = 𝟙 (F.obj A.a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : Limits.IsInitial A<GOAL>F.map ((h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str) = F.map (𝟙 A.a)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : Limits.IsInitial A<GOAL>(h.to { a := F.obj A.a, str := F.map A.str }).f ≫ A.str = 𝟙 A.a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>-↑((o.areaForm x) y) + ↑⟪x, y⟫_ℝ * Complex.I = Complex.I * (↑⟪x, y⟫_ℝ + ↑((o.areaForm x) y) * Complex.I)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<GOAL>Splits φ P.toPoly ↔ ∃ x y z, (map φ P).roots = {x, y, z}
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s s' : Finset α<VAR>hs : Disjoint s s'<VAR>t : Finset β<GOAL>Disjoint (interedges r s t) (interedges r s' t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s s' : Finset α<VAR>hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'<VAR>t : Finset β<GOAL>∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s s' : Finset α<VAR>hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'<VAR>t : Finset β<VAR>a✝ : α × β<VAR>hx : a✝ ∈ interedges r s t<VAR>hy : a✝ ∈ interedges r s' t<GOAL>False
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t✝ t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>s s' : Finset α<VAR>hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'<VAR>t : Finset β<VAR>a✝ : α × β<VAR>hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2<VAR>hy : a✝.1 ∈ s' ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2<GOAL>False
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>n : ℕ<VAR>f : ι → ℕ<GOAL>f ∈ map { toFun := fun m a => Multiset.count a ↑m, inj' := ⋯ } (s.sym n) ↔ f ∈ s.piAntidiag n
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>n : ℕ<VAR>f : ι → ℕ<GOAL>(∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ Multiset.card s_1 = n ∧ ∀ (a : ι), Multiset.count a s_1 = f a) ↔ s.sum f = n ∧ ∀ (i : ι), ¬f i = 0 → i ∈ s
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hR : autoParam (R ⊆ M.E) _auto✝<GOAL>(M ↾ R).Basis I X ↔ M.Basis I X ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hR : autoParam (R ⊆ M.E) _auto✝<GOAL>X ⊆ R → (M.Basis I (X ∩ M.E) ↔ M.Basis I X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<VAR>hR : autoParam (R ⊆ M.E) _auto✝<VAR>hXR : X ⊆ R<GOAL>M.Basis I (X ∩ M.E) ↔ M.Basis I X
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>α : ℝ≥0<VAR>α_hyp : α < rieszContentAux Λ K + ε<VAR>f : X →ᵇ ℝ≥0<VAR>f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α<GOAL>∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>α : ℝ≥0<VAR>α_hyp : α < rieszContentAux Λ K + ε<VAR>f : X →ᵇ ℝ≥0<VAR>f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α<GOAL>Λ f < rieszContentAux Λ K + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>α : ℝ≥0<VAR>α_hyp : α < rieszContentAux Λ K + ε<VAR>f : X →ᵇ ℝ≥0<VAR>f_hyp : f ∈ {f | ∀ x ∈ K, 1 ≤ f x} ∧ Λ f = α<GOAL>α < rieszContentAux Λ K + ε
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ✝ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>x✝ : (α × β) × γ<GOAL>x✝ ∈ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α 0<VAR>p : (j : Fin n) → α (succAbove 0 j)<GOAL>insertNth 0 x p = cons x fun j => _root_.cast ⋯ (p j)
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α 0<VAR>p : (j : Fin n) → α (succAbove 0 j)<GOAL>p = removeNth 0 (cons x fun j => _root_.cast ⋯ (p j))
<VAR>m n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>β : Type v<VAR>x : α 0<VAR>p : (j : Fin n) → α (succAbove 0 j)<VAR>j : Fin n<GOAL>p j = removeNth 0 (cons x fun j => _root_.cast ⋯ (p j)) j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>univ.innerDualCone = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : InnerProductSpace ℝ H<VAR>s t : Set H<GOAL>∀ x ∈ univ.innerDualCone, x = 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.2418, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : Sheaf J E<VAR>Y : Sheaf J D<VAR>A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj<VAR>η : (composeAndSheafify J G).obj X ⟶ Y<GOAL>η.val = sheafifyLift J ((A.homEquiv X.val Y.val).symm ((A.homEquiv X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val))) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.2418, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : Sheaf J E<VAR>Y : Sheaf J D<VAR>A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj<VAR>η : (composeAndSheafify J G).obj X ⟶ Y<GOAL>toSheafify J (X.val ⋙ G) ≫ η.val = (A.homEquiv X.val Y.val).symm ((A.homEquiv X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ η.val))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.2418, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X : Sheaf J E<VAR>Y : Sheaf J D<VAR>A : (whiskeringRight Cᵒᵖ E D).obj G ⊣ (whiskeringRight Cᵒᵖ D E).obj F := Adjunction.whiskerRight Cᵒᵖ adj<VAR>γ : X ⟶ (sheafCompose J F).obj Y<GOAL>(A.homEquiv X.val Y.val) (toSheafify J (X.val ⋙ G) ≫ sheafifyLift J ((A.homEquiv X.val Y.val).symm γ.val) ⋯) = γ.val
<VAR>m : ℕ∞<GOAL>↑m ≤ 1 ↔ m ≤ 1
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 ⋯) f = (setToL1 hT) f + (setToL1 hT') f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>f : ↥(Lp E 1 μ)<GOAL>setToL1 ⋯ = setToL1 hT + setToL1 hT'
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>f : ↥(Lp E 1 μ)<GOAL>(setToL1 hT + setToL1 hT').comp (coeToLp α E ℝ) = setToL1SCLM α E μ ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>((setToL1 hT + setToL1 hT').comp (coeToLp α E ℝ)) f = (setToL1SCLM α E μ ⋯) f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup F'<VAR>inst✝⁵ : NormedSpace ℝ F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT' : DominatedFinMeasAdditive μ T' C'<VAR>f✝ : ↥(Lp E 1 μ)<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>(setToL1 hT) ↑f + (setToL1 hT') ↑f = (setToL1SCLM α E μ ⋯) f
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p / q = p - 1
<VAR>a b p q : ℝ<VAR>h : p.IsConjExponent q<GOAL>p = (p - 1) * q
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p.succAbove i < p ↔ i.castSucc < p
<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.castSucc < p<GOAL>p.succAbove i < p ↔ i.castSucc < p
<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 < i.succ<GOAL>p.succAbove i < p ↔ i.castSucc < p
<VAR>α : Type u_1<VAR>inst✝¹ : Neg α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm (-x) = -(equivShrink α).symm x
<VAR>α : Type u_1<VAR>inst✝¹ : Neg α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm ((equivShrink α).symm.symm (-(equivShrink α).symm x)) = -(equivShrink α).symm x
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto f l atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atBot ↔ Tendsto (Int.cast ∘ f) l atBot
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionSemiring R<VAR>inst✝ : NeZero 2<VAR>a : R<GOAL>(a + a) / 2 = a
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra F L<VAR>ne : Nonempty (K →ₐ[F] L)<VAR>h : Normal F L<VAR>φ : K →ₐ[F] L<GOAL>normalClosure F K L = ⨆ x, adjoin F ((minpoly F x).rootSet L)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra F L<VAR>ne : Nonempty (K →ₐ[F] L)<VAR>h : Normal F L<VAR>φ : K →ₐ[F] L<VAR>x : K<GOAL>Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra F L<VAR>ne : Nonempty (K →ₐ[F] L)<VAR>h : Normal F L<VAR>φ : K →ₐ[F] L<VAR>x : K<GOAL>Splits (algebraMap F L) (minpoly F (φ x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β × γ → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable ((fun x => ∫ (y : γ), (fun u => f (u.1.2, u.2)) (x, y) ∂η x) ∘ fun x => (a, x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>E : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : β × γ → E<VAR>hf : StronglyMeasurable f<GOAL>StronglyMeasurable fun x => ∫ (y : γ), (fun u => f (u.1.2, u.2)) (x, y) ∂η x
<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>hp : ∀ e ∈ p.edges, e ∈ H.edgeSet<VAR>K : SimpleGraph V<VAR>hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet<GOAL>(p.transfer H hp).transfer K hp' = p.transfer K ⋯
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>f : (α → ℕ) → ℕ<GOAL>DiophFn f = DiophPFun ↑f
<VAR>α β γ : Type u<VAR>S S' : Set (α → ℕ)<VAR>f : (α → ℕ) → ℕ<VAR>v : Option α → ℕ<GOAL>v ∈ {v | f (v ∘ some) = v none} ↔ v ∈ {v | (↑f).graph (v ∘ some, v none)}
<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>p : TangentBundle I M<VAR>hg : MDifferentiableAt I' I'' g (f p.proj)<VAR>hf : MDifferentiableAt I I' f p.proj<GOAL>(mfderiv I I'' (g ∘ f) p.proj) p.snd = (mfderiv I' I'' g (f p.proj)) ((mfderiv I I' f p.proj) p.snd)
<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>p : TangentBundle I M<VAR>hg : MDifferentiableAt I' I'' g (f p.proj)<VAR>hf : MDifferentiableAt I I' f p.proj<GOAL>((mfderiv I' I'' g (f p.proj)).comp (mfderiv I I' f p.proj)) p.snd = (mfderiv I' I'' g (f p.proj)) ((mfderiv I I' f p.proj) p.snd)
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>g : α → ℝ≥0∞<VAR>f : ι → α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>q : ℝ<VAR>p : ι → ℝ<VAR>hpq : q + ∑ i ∈ s, p i = 1<VAR>hq : 0 ≤ q<VAR>hp : ∀ i ∈ s, 0 ≤ p i<GOAL>∫⁻ (t : α), ∏ j ∈ insertNone s, (j.elim (g t) fun j => f j t) ^ j.elim q p ∂μ ≤ ∏ j ∈ insertNone s, (∫⁻ (t : α), j.elim (g t) fun j => f j t ∂μ) ^ j.elim q p
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>g : α → ℝ≥0∞<VAR>f : ι → α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>q : ℝ<VAR>p : ι → ℝ<VAR>hpq : q + ∑ i ∈ s, p i = 1<VAR>hq : 0 ≤ q<VAR>hp : ∀ i ∈ s, 0 ≤ p i<GOAL>∀ i ∈ insertNone s, AEMeasurable (fun t => i.elim (g t) fun j => f j t) μ
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>g : α → ℝ≥0∞<VAR>f : ι → α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>q : ℝ<VAR>p : ι → ℝ<VAR>hpq : q + ∑ i ∈ s, p i = 1<VAR>hq : 0 ≤ q<VAR>hp : ∀ i ∈ s, 0 ≤ p i<GOAL>∑ i ∈ insertNone s, i.elim q p = 1
<VAR>α✝ : Type u_1<VAR>inst✝¹ : MeasurableSpace α✝<VAR>μ✝ : Measure α✝<VAR>α : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Finset ι<VAR>g : α → ℝ≥0∞<VAR>f : ι → α → ℝ≥0∞<VAR>hg : AEMeasurable g μ<VAR>hf : ∀ i ∈ s, AEMeasurable (f i) μ<VAR>q : ℝ<VAR>p : ι → ℝ<VAR>hpq : q + ∑ i ∈ s, p i = 1<VAR>hq : 0 ≤ q<VAR>hp : ∀ i ∈ s, 0 ≤ p i<GOAL>∀ i ∈ insertNone s, 0 ≤ i.elim q p
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>l : List α<GOAL>(a ::ₘ ⟦l⟧).powerset = powerset ⟦l⟧ + map (cons a) (powerset ⟦l⟧)
<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 : HasMFDerivAt I' I'' g (f x) g'<VAR>hf : HasMFDerivAt I I' f x f'<GOAL>HasMFDerivAt I I'' (g ∘ f) 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 univ (f x) g'<VAR>hf : HasMFDerivWithinAt I I' f univ x f'<GOAL>HasMFDerivWithinAt I I'' (g ∘ f) univ x (g'.comp f')
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : CommRing S<VAR>inst✝¹² : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝¹¹ : CommRing R'<VAR>inst✝¹⁰ : CommRing S'<VAR>inst✝⁹ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝⁸ : Algebra R R'<VAR>inst✝⁷ : Algebra S S'<VAR>inst✝⁶ : Algebra R S'<VAR>inst✝⁵ : IsScalarTower R R' S'<VAR>inst✝⁴ : IsScalarTower R S S'<VAR>T : Type uT<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>i : P.vars<GOAL>P.toKaehler (P.cotangentSpaceBasis i) = (D R S) (P.val i)