ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>f : ℕ → ℕ →. ℕ<VAR>h : _root_.Partrec fun v => f v.head v.tail.head<VAR>v : ℕ × ℕ<GOAL>f (v.1 ::ᵥ v.2 ::ᵥ nil).head (v.1 ::ᵥ v.2 ::ᵥ nil).tail.head = f v.1 v.2
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f s x<VAR>n : ℕ∞<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>h : AnalyticWithinAt 𝕜 f s x<VAR>n : ℕ∞<VAR>g : E → F<VAR>fx : f x = g x<VAR>fg : f =ᶠ[𝓝[s] x] g<VAR>hg : AnalyticAt 𝕜 g x<GOAL>ContDiffWithinAt 𝕜 n f s x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => f x / r) l atTop ↔ r < 0
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝⁶ : Presheaf.IsLocallyInjective J α<VAR>inst✝⁵ : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝⁴ : Presheaf.IsLocallyInjective J φ<VAR>inst✝³ : Presheaf.IsLocallySurjective J φ<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>M₀' : PresheafOfModules R₀<VAR>A' : Sheaf J AddCommGrp<VAR>φ' : M₀'.presheaf ⟶ A'.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ'<VAR>inst✝ : Presheaf.IsLocallySurjective J φ'<VAR>τ₀ : M₀ ⟶ M₀'<VAR>τ : A ⟶ A'<VAR>fac : τ₀.hom ≫ φ' = φ ≫ τ.val<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.val.obj X)) (x : ↑((sheafify α φ).val.presheaf.obj X)), (τ.val.app X) (r • x) = r • (τ.val.app X) x
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝⁶ : Presheaf.IsLocallyInjective J α<VAR>inst✝⁵ : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝⁴ : Presheaf.IsLocallyInjective J φ<VAR>inst✝³ : Presheaf.IsLocallySurjective J φ<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>M₀' : PresheafOfModules R₀<VAR>A' : Sheaf J AddCommGrp<VAR>φ' : M₀'.presheaf ⟶ A'.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ'<VAR>inst✝ : Presheaf.IsLocallySurjective J φ'<VAR>τ₀ : M₀ ⟶ M₀'<VAR>τ : A ⟶ A'<VAR>fac : τ₀.hom ≫ φ' = φ ≫ τ.val<VAR>f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.val.obj X)) (x : ↑((sheafify α φ).val.presheaf.obj X)), (τ.val.app X) (r • x) = r • (τ.val.app X) x
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝⁶ : Presheaf.IsLocallyInjective J α<VAR>inst✝⁵ : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝⁴ : Presheaf.IsLocallyInjective J φ<VAR>inst✝³ : Presheaf.IsLocallySurjective J φ<VAR>inst✝² : J.WEqualsLocallyBijective AddCommGrp<VAR>M₀' : PresheafOfModules R₀<VAR>A' : Sheaf J AddCommGrp<VAR>φ' : M₀'.presheaf ⟶ A'.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ'<VAR>inst✝ : Presheaf.IsLocallySurjective J φ'<VAR>τ₀ : M₀ ⟶ M₀'<VAR>τ : A ⟶ A'<VAR>fac : τ₀.hom ≫ φ' = φ ≫ τ.val<VAR>f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')<VAR>eq : τ.val = f.hom<GOAL>∀ (X : Cᵒᵖ) (r : ↑(R.val.obj X)) (x : ↑((sheafify α φ).val.presheaf.obj X)), (τ.val.app X) (r • x) = r • (τ.val.app X) x
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁✝ π₂✝ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π₁ π₂ : Prepartition I<GOAL>(π₁ ⊓ π₂).iUnion = π₁.iUnion ∩ π₂.iUnion
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : ConcreteCategory C<VAR>J : Type w<VAR>F : J → C<VAR>inst✝¹ : HasProduct F<VAR>inst✝ : PreservesLimit (Discrete.functor F) (forget C)<VAR>x : (j : J) → (forget C).obj (F j)<VAR>j : J<GOAL>(Pi.π F j) ((productEquiv F).symm x) = x j
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Finite ι<VAR>x : E<GOAL>∃! v, v +ᵥ x ∈ fundamentalDomain b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>inst✝¹ : FloorRing K<VAR>inst✝ : Finite ι<VAR>x : E<VAR>val✝ : Fintype ι<GOAL>∃! v, v +ᵥ x ∈ fundamentalDomain b
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<VAR>F' : MonoFactorisation f<VAR>x : ↑(image f)<GOAL>(F'.e ≫ F'.m) ↑(Classical.indefiniteDescription (fun x_1 => f x_1 = ↑x) ⋯) = (ι f) x
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>G H : ModuleCat R<VAR>f : G ⟶ H<VAR>F' : MonoFactorisation f<VAR>x : ↑(image f)<GOAL>↑x = (ι f) x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>one_mem : 1 ∈ s<VAR>div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s<VAR>a : G<VAR>ha : a ∈ s<VAR>this : 1 * a⁻¹ ∈ s<GOAL>a⁻¹ = 1 * a⁻¹
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>one_mem : 1 ∈ s<VAR>div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s<VAR>inv_mem : ∀ a ∈ s, a⁻¹ ∈ s<VAR>a b : G<VAR>ha : a ∈ s<VAR>hb : b ∈ s<VAR>this : a * b⁻¹⁻¹ ∈ s<GOAL>b = b⁻¹⁻¹
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid N₂<VAR>inst✝⁴ : Module R N₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>M : Matrix n m N₂<VAR>i✝¹ : n<VAR>i✝ : m<GOAL>(((toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M ∘ₗ single i✝¹) 1 ∘ₗ single i✝) 1 = (((toLinearMap₂' R) M ∘ₗ single i✝¹) 1 ∘ₗ single i✝) 1
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → B ⟶ objs j<VAR>inst✝ : HasWidePushout B objs arrows<VAR>X : C<VAR>f : B ⟶ X<VAR>fs : (j : J) → objs j ⟶ X<VAR>w : ∀ (j : J), arrows j ≫ fs j = f<GOAL>head arrows ≫ desc f fs w = f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝² : (i : α) → NormedAddCommGroup (E i)<VAR>I : Type u_3<VAR>B : I → Type u_4<VAR>inst✝¹ : (i : I) → NormedRing (B i)<VAR>inst✝ : ∀ (i : I), NormOneClass (B i)<VAR>i : I<GOAL>(fun i => ‖1 i‖) i ≤ 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x ≤ g x<VAR>n : ℕ<GOAL>f^[n] x ≤ g^[n] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x ≤ g x<VAR>n : ℕ<GOAL>f^[0] x ≤ g^[0] x
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x ≤ g x<VAR>n : ℕ<GOAL>∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : Monotone g<VAR>x : α<VAR>hx : f x ≤ g x<VAR>n : ℕ<GOAL>∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
<VAR>α : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>k : α<VAR>h : ∀ (x : α), k * x = 0 → x = 0<GOAL>IsLeftRegular k
<VAR>α : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>k : α<VAR>h : ∀ (x : α), k * x = 0 → x = 0<VAR>x y : α<VAR>h' : k * x = k * y<GOAL>k * (x - y) = 0
<VAR>m n✝ a✝ b✝ c d : ℤ<VAR>a b n : ℕ<GOAL>↑a % ↑n = ↑b % ↑n ↔ a % n = b % n
<VAR>m n✝ a✝ b✝ c d : ℤ<VAR>a b n : ℕ<GOAL>↑a % ↑n = ↑b % ↑n ↔ ↑(a % n) = ↑(b % n)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>x : G<GOAL>comap (fun x_1 => x_1 / x) (𝓝 1) = 𝓝 x
<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∞<GOAL>⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ 0), 𝓟 (Iio a)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝⁶ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝⁵ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝⁴ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) (restrict g ⋯) = 0<GOAL>(trace R M) (g ∘ₗ f) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝⁶ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝⁵ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝⁴ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) (restrict g ⋯) = 0<VAR>hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)<GOAL>(trace R M) (g ∘ₗ f) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝⁶ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝⁵ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝⁴ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) (restrict g ⋯) = 0<VAR>hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)<GOAL>∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) ((g ∘ₗ f).restrict ⋯) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝⁶ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝⁵ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝⁴ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) (restrict g ⋯) = 0<VAR>hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)<VAR>μ : R<GOAL>(trace R ↥(⨆ k, (f.genEigenspace μ) k)) ((g ∘ₗ f).restrict ⋯) = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝⁶ : DecidableEq ι<VAR>h : IsInternal N<VAR>inst✝⁵ : ∀ (i : ι), Module.Finite R ↥(N i)<VAR>inst✝⁴ : ∀ (i : ι), Module.Free R ↥(N i)<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsPrincipalIdealRing R<VAR>inst✝¹ : Module.Free R M<VAR>inst✝ : Module.Finite R M<VAR>f g : Module.End R M<VAR>h_comm✝ : Commute f g<VAR>hf : ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>hg : ∀ (μ : R), (trace R ↥(⨆ k, (f.genEigenspace μ) k)) (restrict g ⋯) = 0<VAR>hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(⨆ k, (f.genEigenspace μ) k) ↑(⨆ k, (f.genEigenspace μ) k)<VAR>μ : R<VAR>h_comm : Commute (restrict g ⋯) (restrict f ⋯)<GOAL>(trace R ↥(⨆ k, (f.genEigenspace μ) k)) ((g ∘ₗ f).restrict ⋯) = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Semigroup P<VAR>f : M →ₙ* P<VAR>g : N →ₙ* P<VAR>comm : ∀ (m : M) (n : N), Commute (f m) (g n)<VAR>mn mn' : M × N<GOAL>(fun mn => f mn.1 * g mn.2) (mn * mn') = (fun mn => f mn.1 * g mn.2) mn * (fun mn => f mn.1 * g mn.2) mn'
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I X R✝ J E R : Set α<GOAL>loopyOn E ↾ R = loopyOn R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I X R✝ J E R : Set α<GOAL>∀ I ⊆ (loopyOn E ↾ R).E, (loopyOn E ↾ R).Indep I ↔ (loopyOn R).Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E✝ B I X R✝ J E R : Set α<GOAL>∀ I ⊆ R, I = ∅ → I ⊆ R
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>(‖2 • z + y‖ * ‖2 • z + y‖ - ‖y - 2 • z‖ * ‖y - 2 • z‖) / 2 = ‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖
<VAR>𝕜 : Type u_1<VAR>inst✝³ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : InnerProductSpaceable E<VAR>y z : E<GOAL>(2 * (‖y + z‖ * ‖y + z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖ - (2 * (‖y - z‖ * ‖y - z‖ + ‖z‖ * ‖z‖) - ‖y‖ * ‖y‖)) / 2 = ‖y + z‖ * ‖y + z‖ - ‖y - z‖ * ‖y - z‖
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w : List (Symbol T N)<VAR>hvw : r.Rewrites v w<VAR>p : List (Symbol T N)<GOAL>r.Rewrites (p ++ v) (p ++ w)
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w : List (Symbol T N)<VAR>hvw : ∃ p q, v = p ++ [Symbol.nonterminal r.input] ++ q ∧ w = p ++ r.output ++ q<VAR>p : List (Symbol T N)<GOAL>∃ p_1 q, p ++ v = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ w = p_1 ++ r.output ++ q
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w p x y : List (Symbol T N)<VAR>hxy : v = x ++ [Symbol.nonterminal r.input] ++ y ∧ w = x ++ r.output ++ y<GOAL>∃ p_1 q, p ++ v = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ p ++ w = p_1 ++ r.output ++ q
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w p x y : List (Symbol T N)<VAR>hxy : v = x ++ [Symbol.nonterminal r.input] ++ y ∧ w = x ++ r.output ++ y<GOAL>p ++ v = p ++ x ++ [Symbol.nonterminal r.input] ++ y ∧ p ++ w = p ++ x ++ r.output ++ y
<VAR>M✝ : Type u_2<VAR>inst✝⁷ : AddCommGroup M✝<VAR>K✝ : Type u_3<VAR>inst✝⁶ : Field K✝<VAR>inst✝⁵ : Module K✝ M✝<VAR>f✝ : End K✝ M✝<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>K : Type u_3<VAR>inst✝¹ : Field K<VAR>inst✝ : Module K M<VAR>f g : End K M<VAR>t : K<VAR>h : f.IsSemisimple<VAR>ht : t ≠ 0<GOAL>(t • f).IsSemisimple
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>convexBodySumFun (x + y) ≤ convexBodySumFun x + convexBodySumFun y
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x y : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>∑ w : InfinitePlace K, ↑w.mult * (normAtPlace w) (x + y) ≤ ∑ x_1 : InfinitePlace K, ↑x_1.mult * ((normAtPlace x_1) x + (normAtPlace x_1) y)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<GOAL>IsJacobson R ↔ ∀ (P : Ideal R), P.IsPrime → P.jacobson = P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<GOAL>(∀ (P : Ideal R), P.IsPrime → P.jacobson = P) → ∀ (I : Ideal R), I.IsRadical → I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : x ∈ I.jacobson<GOAL>x ∈ I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : x ∈ I.jacobson<GOAL>∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsPrime} → x ∈ I_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : x ∈ I.jacobson<VAR>P : Ideal R<VAR>hP : P ∈ {J | I ≤ J ∧ J.IsPrime}<GOAL>x ∈ P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : x ∈ I.jacobson<VAR>P : Ideal R<VAR>hP : I ≤ P ∧ P.IsPrime<GOAL>x ∈ P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1<VAR>P : Ideal R<VAR>hP : I ≤ P ∧ P.IsPrime<GOAL>x ∈ P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I✝ : Ideal R<VAR>h : ∀ (P : Ideal R), P.IsPrime → P.jacobson = P<VAR>I : Ideal R<VAR>hI : I.IsRadical<VAR>x : R<VAR>hx : ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x ∈ I_1<VAR>P : Ideal R<VAR>hP : I ≤ P ∧ P.IsPrime<GOAL>∀ ⦃I : Ideal R⦄, I ∈ {J | P ≤ J ∧ J.IsMaximal} → x ∈ I
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k<GOAL>∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k<GOAL>(u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k<VAR>this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k<GOAL>(u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu : Monotone u<VAR>n : ℕ<VAR>ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k<VAR>this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k<GOAL>(u (n + 1) - u n) • f (u (n + 1)) = ∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>((f.extend I).symm ≫ f'.extend I).source = ↑I '' (f.symm ≫ₕ f').source
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : TopologicalSpace H<VAR>inst✝⁴ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : NormedSpace 𝕜 E'<VAR>inst✝¹ : TopologicalSpace H'<VAR>inst✝ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<GOAL>↑I.symm ⁻¹' f.target ∩ ↑(f.extend I).symm ⁻¹' f'.source ∩ range ↑I = ↑I.symm ⁻¹' (f.symm ≫ₕ f').source ∩ range ↑I
<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>x y : V<GOAL>⊤.Reachable x y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module.Finite R M₁<VAR>inst✝⁴ : Module.Free R M₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module.Finite R M₂<VAR>inst✝ : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>e : M₁ ≃ₗ[R] M₂<VAR>φ : Module.End R M₁<VAR>b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁<GOAL>LinearMap.charpoly (e.conj φ) = LinearMap.charpoly φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module.Finite R M₁<VAR>inst✝⁴ : Module.Free R M₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module.Finite R M₂<VAR>inst✝ : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>e : M₁ ≃ₗ[R] M₂<VAR>φ : Module.End R M₁<VAR>b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁<GOAL>((LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ)).charpoly = ((LinearMap.toMatrix b b) φ).charpoly
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module.Free R M<VAR>inst✝⁸ : Module.Finite R M<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R M₁<VAR>inst✝⁵ : Module.Finite R M₁<VAR>inst✝⁴ : Module.Free R M₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : Module.Finite R M₂<VAR>inst✝ : Module.Free R M₂<VAR>f : M →ₗ[R] M<VAR>e : M₁ ≃ₗ[R] M₂<VAR>φ : Module.End R M₁<VAR>b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁<VAR>i j : ChooseBasisIndex R M₁<GOAL>(LinearMap.toMatrix (b.map e) (b.map e)) (e.conj φ) i j = (LinearMap.toMatrix b b) φ i j
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>X Y Z : C<VAR>f✝ : Y ⟶ X<VAR>S R : Sieve X<VAR>f : Y ⟶ X<GOAL>S.arrows f ↔ pullback f S = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁶ : SemilatticeSup α<VAR>inst✝⁵ : OrderTop α<VAR>inst✝⁴ : DecidableRel fun x x_1 => x ≤ x_1<VAR>inst✝³ : SemilatticeSup β<VAR>inst✝² : BoundedOrder β<VAR>inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>hs : a ∉ lowerClosure ↑s<VAR>ht : a ∈ lowerClosure ↑t<GOAL>(s ∪ t).truncatedSup a = t.truncatedSup a