ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>s : String<VAR>p : Char → Bool<GOAL>s.all p = s.data.all p
<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>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.sheafify P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ<GOAL>η = γ
<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>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.sheafify P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ<GOAL>J.toPlus (J.plusObj P) ≫ η = J.toPlus (J.plusObj P) ≫ γ
<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>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.sheafify P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ<GOAL>J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ η = J.toPlus P ≫ J.toPlus (J.plusObj P) ≫ γ
<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>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η γ : J.sheafify P ⟶ Q<VAR>hQ : Presheaf.IsSheaf J Q<VAR>h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ<GOAL>(J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ η = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Icc a b = ∅ ↔ ¬a ≤ b
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>hm : m ≤ M.M i i' * 2<GOAL>cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>hm : m ≤ M.M i i' * 2<GOAL>(if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2) = (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((M.M i i' * 2 - m) / 2)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>hm : m ≤ M.M i i' * 2<GOAL>(if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (↑m / ↑2) = (if Even (↑(M.M i i' * 2) - ↑m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i' * 2) - ↑m) / ↑2)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>m' : ℤ<GOAL>(if Even m' then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m' / 2) = (if Even (↑(M.M i i') * 2 - m') then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - m') / 2)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>k : ℤ<GOAL>(if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) = (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>m : ℕ<VAR>k : ℤ<GOAL>(if Even (2 * k + 1) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ ((2 * k + 1) / 2) = (if Even (↑(M.M i i') * 2 - (2 * k + 1)) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - (2 * k + 1)) / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>x : β<GOAL>x ∈ (insert a s).biUnion t ↔ x ∈ t a ∪ s.biUnion t
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<GOAL>eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂0, ‖f x‖₊ ≤ C<GOAL>eLpNorm f p 0 ≤ C • 0 Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<VAR>hμ : NeZero μ<GOAL>eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<VAR>hμ : NeZero μ<VAR>hp : ¬p = 0<GOAL>eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<VAR>hμ : NeZero μ<VAR>hp : ¬p = 0<VAR>this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊<GOAL>eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>C : ℝ≥0<VAR>hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C<VAR>hμ : NeZero μ<VAR>hp : ¬p = 0<VAR>this : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖↑C‖₊<GOAL>eLpNorm (fun x => ↑C) p μ = C • μ Set.univ ^ p.toReal⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>(s.erase a).Nonempty ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>(∃ x ∈ s, x ≠ a) ↔ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>(∃ x ∈ s, x ≠ a) → s.Nontrivial
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>c : CokernelCofork (f - g)<GOAL>f ≫ Cofork.π c = g ≫ Cofork.π c
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>l ⊆ l
<VAR>α : Type u_1<VAR>l : Lists' α true<GOAL>ofList l.toList ⊆ ofList l.toList
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>W X X' Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ Y<GOAL>f ≫ g ≫ e.unit.app Y = f' ≫ g' ≫ e.unit.app Y ↔ f ≫ g = f' ≫ g'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f✝ g✝ : α → β<VAR>μ ν : Measure α<VAR>g : β → γ<VAR>f : α → β<VAR>hg : AEMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(Measure.map g (Measure.map f μ)) s = (Measure.map (g ∘ f) μ) s
<VAR>α : Type u_1<VAR>β : ?m.4523<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsLower α<VAR>s : Set α<GOAL>IsOpen s ↔ GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>f : F<GOAL>HasStrictDerivAt (fun y => c y • f) (c' • f) x
<VAR>𝕜 : Type u<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>G : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>inst✝⁴ : NormedSpace 𝕜 G<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>c : 𝕜 → 𝕜'<VAR>c' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>f : F<VAR>this : HasStrictDerivAt (fun y => c y • f) (c x • 0 + c' • f) x<GOAL>HasStrictDerivAt (fun y => c y • f) (c' • f) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : (of R M) m ∈ span R ↑(closure (⇑(of R M) '' S))<GOAL>m ∈ closure S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : (of R M) m ∈ span R ↑(Submonoid.map (of R M) (closure S))<GOAL>m ∈ closure S
<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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffAt 𝕜 n f 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>X : Type u_2<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>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : Subsingleton F<GOAL>ContDiffAt 𝕜 n (fun x => 0) 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))<GOAL>MDifferentiableOn I I' f univ ↔ MDifferentiable I I' 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))<GOAL>(∀ (x : M), MDifferentiableAt I I' f x) ↔ MDifferentiable I I' f
<VAR>θ : ℝ<GOAL>(↑θ).toReal = θ - 2 * π ↔ θ ∈ Set.Ioc π (3 * π)
<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>inst✝ : Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<GOAL>∃ a b, ↑x = ↑a + b • y
<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>inst✝ : Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>mem1 : ↑x ∈ ↑(supExtensionOfMaxSingleton i f y)<GOAL>∃ a b, ↑x = ↑a + b • y
<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>inst✝ : Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>mem1 : ↑x ∈ ↑(extensionOfMax i f).domain + ↑(Submodule.span R {y})<GOAL>∃ a b, ↑x = ↑a + b • y
<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>inst✝ : Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>a : N<VAR>a_mem : a ∈ ↑(extensionOfMax i f).domain<VAR>b : N<VAR>b_mem : b ∈ Submodule.span R {y}<VAR>eq1 : (fun x x_1 => x + x_1) a b = ↑x<GOAL>∃ a b, ↑x = ↑a + b • y
<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>inst✝ : Fact (Function.Injective ⇑i)<VAR>y : N<VAR>x : ↥(supExtensionOfMaxSingleton i f y)<VAR>a : N<VAR>a_mem : a ∈ ↑(extensionOfMax i f).domain<VAR>b : N<VAR>b_mem : ∃ a, a • y = b<VAR>eq1 : (fun x x_1 => x + x_1) a b = ↑x<GOAL>∃ a b, ↑x = ↑a + b • y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>f : R<GOAL>f ∈ vanishingIdeal (zeroLocus ↑I) ↔ f ∈ I.radical
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>I : Ideal R<VAR>f : R<GOAL>(∀ x ∈ zeroLocus ↑I, f ∈ x.asIdeal) ↔ ∀ p ∈ {J | I ≤ J ∧ J.IsPrime}, f ∈ p
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>n r : Nat<VAR>a : α<VAR>c : HeapNode α<VAR>s : Heap α<VAR>h : WF le n (cons r a c s)<GOAL>WF le 0 (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>n r : Nat<VAR>a : α<VAR>c : HeapNode α<VAR>s : Heap α<VAR>h : WF le n (cons r a c s)<VAR>this : FindMin.WF le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s })<GOAL>WF le 0 (Heap.merge le (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).node.toHeap ((Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).before (Heap.findMin le (cons r a c) s { before := id, val := a, node := c, next := s }).next))
<VAR>α : Type u_1<VAR>le : α → α → Bool<VAR>n r : Nat<VAR>a : α<VAR>c : HeapNode α<VAR>s : Heap α<VAR>h : WF le n (cons r a c s)<VAR>before : Heap α → Heap α<VAR>val : α<VAR>node : HeapNode α<VAR>next : Heap α<VAR>rank✝ : Nat<VAR>hk : ∀ {s : Heap α}, WF le rank✝ s → WF le 0 ({ before := before, val := val, node := node, next := next }.before s)<VAR>ih₁ : HeapNode.WF le { before := before, val := val, node := node, next := next }.val { before := before, val := val, node := node, next := next }.node rank✝<VAR>ih₂ : WF le (rank✝ + 1) { before := before, val := val, node := node, next := next }.next<GOAL>WF le 0 (Heap.merge le { before := before, val := val, node := node, next := next }.node.toHeap ({ before := before, val := val, node := node, next := next }.before { before := before, val := val, node := node, next := next }.next))
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Path u v<VAR>p' : Path u' v'<GOAL>cast hu hv p = p' ↔ HEq p p'
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Path u v<VAR>p' : Path u' v'<GOAL>_root_.cast ⋯ p = p' ↔ HEq p p'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<VAR>hmain : (∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))) ↔ ∀ (p : E × NormedSpace.Dual 𝕜 F), Tendsto (fun a => p.2 ((f a) p.1)) l (𝓝 (p.2 (A p.1)))<GOAL>Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<VAR>hmain : (∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Tendsto (fun a => y ((f a) x)) l (𝓝 (y (A x)))) ↔ ∀ (p : E × NormedSpace.Dual 𝕜 F), Tendsto (fun a => p.2 ((f a) p.1)) l (𝓝 (p.2 (A p.1)))<GOAL>Tendsto (⇑(inducingFn 𝕜 E F) ∘ f) l (𝓝 ((inducingFn 𝕜 E F) A)) ↔ Tendsto (fun a p => p.2 ((f a) p.1)) l (𝓝 fun p => p.2 (A p.1))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>i : ℕ<GOAL>i ∈ (p.toSubring T hp).support ↔ i ∈ p.support
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>i : ℕ<GOAL>(p.toSubring T hp).coeff i = 0 ↔ p.coeff i = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>p : R[X]<VAR>T : Subring R<VAR>hp : ↑p.coeffs ⊆ ↑T<VAR>i : ℕ<GOAL>(p.toSubring T hp).coeff i = 0 ↔ ↑((p.toSubring T hp).coeff i) = 0
<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>ι : Sort u_4<VAR>p : ι → Prop<VAR>h : ∃ i, p i<VAR>f : ι → ℝ≥0∞<GOAL>a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>q n : ℕ<VAR>hprime : Nat.Prime q<VAR>hchar✝ : CharP F q<VAR>this : Fact (Nat.Prime q)<GOAL>((expand F (q ^ n)) f).natSepDegree = f.natSepDegree
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α<VAR>i j : Fin 2<GOAL>(!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) i j = !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → β<VAR>ι : Sort u_2<VAR>g : β → γ<VAR>t₁ : TopologicalSpace α<VAR>t₂ : TopologicalSpace γ<GOAL>Continuous g ↔ Continuous (g ∘ f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>inst✝² : Fintype α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : Fintype { a // p a }<GOAL>Multiset.map Subtype.val univ.val = (filter p univ).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : Fintype α<VAR>s t : Finset α<VAR>inst✝² : Fintype α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : Fintype { a // p a }<GOAL>(map (Embedding.subtype p) univ).val = (filter p univ).val
<VAR>T : Type u<VAR>inst✝¹ : Category.{v, u} T<VAR>f g : Arrow T<VAR>sq : f ⟶ g<VAR>inst✝ : IsIso sq<GOAL>sq.right ≫ (inv sq).right = 𝟙 f.right
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : Quotient (QuotientGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q<VAR>q : Quotient (QuotientGroup.rightRel H)<GOAL>↑((toEquiv ⋯) q) = f q
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : Quotient (QuotientGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q<VAR>q : Quotient (QuotientGroup.rightRel H)<GOAL>(toEquiv ⋯) q = ⟨f q, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<VAR>hf : ∀ (j : Fin b), f (natAdd a j) = 1<GOAL>∏ i : Fin (a + b), f i = ∏ i : Fin a, f (castLE ⋯ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>inst✝ : CommMonoid M<VAR>a b : ℕ<VAR>f : Fin (a + b) → M<VAR>hf : ∀ (j : Fin b), f (natAdd a j) = 1<GOAL>∏ i : Fin a, f (castAdd b i) = ∏ i : Fin a, f (castLE ⋯ i)
<VAR>ι : Type ?u.54871<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁶ : LinearOrder ι<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>inst✝ : Module.Free R M<VAR>Q : QuadraticMap R M N<GOAL>∃ a, a.toQuadraticMap = Q