ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<VAR>V₁ : C<VAR>iVW : V₁ ⟶ W<VAR>iV₁Y₁ : V₁ ⟶ Y₁<VAR>e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁<VAR>V₂ : C<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂Y₂ : V₂ ⟶ Y₂<VAR>e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂<GOAL>∀ ⦃Z_1 : C⦄ (j : Z_1 ⟶ V₂), j ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = j ≫ iV₂Y₂ ≫ g₂ → ℱ.val.map (G.map j).op (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))))) = ℱ.val.map (G.map j).op (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<VAR>V₁ : C<VAR>iVW : V₁ ⟶ W<VAR>iV₁Y₁ : V₁ ⟶ Y₁<VAR>e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁<VAR>V₂ : C<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂Y₂ : V₂ ⟶ Y₂<VAR>e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂<VAR>V₃ : C<VAR>iV₃ : V₃ ⟶ V₂<VAR>e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂<GOAL>ℱ.val.map (G.map iV₃).op (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₁.op (x g₁ hg₁))))) = ℱ.val.map (G.map iV₃).op (ℱ.val.map (G.map iV₂V₁).op (ℱ.val.map (G.map iVW).op (ℱ.val.map i.op (ℱ.val.map f₂.op (x g₂ hg₂)))))
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.131985, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝³ : Category.{?u.132037, u_4} A<VAR>G : C ⥤ D<VAR>inst✝² : G.IsCoverDense K<VAR>inst✝¹ : G.IsLocallyFull K<VAR>ℱ✝ : Dᵒᵖ ⥤ A<VAR>ℱ' : Sheaf K A<VAR>inst✝ : G.IsLocallyFaithful K<VAR>ℱ : SheafOfTypes K<VAR>Z : C<VAR>T : Presieve Z<VAR>x : FamilyOfElements (G.op ⋙ ℱ.val) T<VAR>hx : x.Compatible<VAR>Y₁ Y₂ : C<VAR>X : D<VAR>f₁ : X ⟶ G.obj Y₁<VAR>f₂ : X ⟶ G.obj Y₂<VAR>g₁ : Y₁ ⟶ Z<VAR>g₂ : Y₂ ⟶ Z<VAR>hg₁ : T g₁<VAR>hg₂ : T g₂<VAR>eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂<VAR>W : C<VAR>i : G.obj W ⟶ X<VAR>V₁ : C<VAR>iVW : V₁ ⟶ W<VAR>iV₁Y₁ : V₁ ⟶ Y₁<VAR>e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁<VAR>V₂ : C<VAR>iV₂V₁ : V₂ ⟶ V₁<VAR>iV₂Y₂ : V₂ ⟶ Y₂<VAR>e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂<VAR>V₃ : C<VAR>iV₃ : V₃ ⟶ V₂<VAR>e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂<GOAL>ℱ.val.map (G.map (iV₃ ≫ iV₂V₁ ≫ iV₁Y₁)).op (x g₁ hg₁) = ℱ.val.map (G.map (iV₃ ≫ iV₂Y₂)).op (x g₂ hg₂)
<VAR>m n a : Nat<VAR>cmn : m.Coprime n<VAR>dvd : a ∣ m<GOAL>(m / a).Coprime n
<VAR>G : Type u<VAR>inst✝ : AddCommGroup G<VAR>hG : AddGroup.FG G<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u<VAR>inst✝ : AddCommGroup G<VAR>hG : AddGroup.FG G<VAR>n : ℕ<VAR>ι : Type<VAR>fι : Fintype ι<VAR>p : ι → ℤ<VAR>hp : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Nat.Prime (p i)), ∃ e, Nonempty (G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod (p i ^ e i))
<VAR>G : Type u<VAR>inst✝ : AddCommGroup G<VAR>hG : AddGroup.FG G<VAR>n : ℕ<VAR>ι : Type<VAR>fι : Fintype ι<VAR>p : ι → ℤ<VAR>hp : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>f : G ≃ₗ[ℤ] (Fin n →₀ ℤ) × ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<GOAL>G ≃+ (Fin n →₀ ℤ) × ⨁ (i : ι), ZMod ((fun i => (p i).natAbs) i ^ e i)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>hmn : ↑m < n<VAR>hs : UniqueDiffOn 𝕜 (insert x s)<GOAL>DifferentiableWithinAt 𝕜 (iteratedDerivWithin m f s) s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<VAR>a : α<VAR>b : β<GOAL>(a, b) ∈ l₁ ×ˢ l₂ ↔ a ∈ l₁ ∧ b ∈ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : autoParam s.Finite _auto✝<GOAL>(s \ {a}).ncard + 1 = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : autoParam s.Finite _auto✝<GOAL>↑(s \ {a}).ncard + 1 = ↑s.ncard
<VAR>α : Type u<VAR>s : Set α<VAR>c : Cardinal.{u}<GOAL>#{ t // t ⊆ s ∧ #↑t ≤ c } ≤ max #↑s ℵ₀ ^ c
<VAR>α : Type u<VAR>s : Set α<VAR>c : Cardinal.{u}<GOAL>#{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }
<VAR>α : Type u<VAR>s : Set α<VAR>c : Cardinal.{u}<VAR>t : Set α<VAR>left✝ : t ⊆ s<VAR>h2t : #↑t ≤ c<GOAL>{ toFun := fun t => Subtype.val ⁻¹' ↑t, inj' := ⋯ } ⟨t, ⋯⟩ ∈ fun t => Quot.lift ((fun α β => Nonempty (α ↪ β)) ↑t) ⋯ c
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>I : Ideal A<VAR>inst✝ : Algebra R A<VAR>a₁✝ : R ⧸ comap (algebraMap R A) I<VAR>a : R<VAR>a₂✝ : R ⧸ comap (algebraMap R A) I<VAR>b : R<VAR>hab : (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r a) = (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r b)<GOAL>Quot.mk Setoid.r a = Quot.mk Setoid.r b
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>I : Ideal A<VAR>inst✝ : Algebra R A<VAR>a₁✝ : R ⧸ comap (algebraMap R A) I<VAR>a : R<VAR>a₂✝ : R ⧸ comap (algebraMap R A) I<VAR>b : R<VAR>hab : (algebraMap R A) a - (algebraMap R A) b ∈ I<GOAL>Quot.mk Setoid.r a = Quot.mk Setoid.r b
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : CommRing A<VAR>inst✝² : Algebra R₁ A<VAR>inst✝¹ : Algebra R₂ A<VAR>I : Ideal A<VAR>inst✝ : Algebra R A<VAR>a₁✝ : R ⧸ comap (algebraMap R A) I<VAR>a : R<VAR>a₂✝ : R ⧸ comap (algebraMap R A) I<VAR>b : R<VAR>hab : (algebraMap R A) (a - b) ∈ I<GOAL>Quot.mk Setoid.r a = Quot.mk Setoid.r b
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<GOAL>padicNorm p ↑m = 1 ↔ ¬↑p ∣ m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<GOAL>padicNorm p ↑m = 1 ↔ ¬↑(p ^ 1) ∣ m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℤ<GOAL>padicNorm p ↑m = 1 ↔ (↑p)⁻¹ < padicNorm p ↑m
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<VAR>α : Type u_6<VAR>l : Filter α<VAR>f : α → Z<VAR>z : Z<VAR>hz : z ∈ e.source<GOAL>Tendsto f l (𝓝 z) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace F<VAR>proj : Z → B<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace (TotalSpace F E)<VAR>e : Trivialization F proj<VAR>x : Z<VAR>α : Type u_6<VAR>l : Filter α<VAR>f : α → Z<VAR>z : Z<VAR>hz : z ∈ e.source<GOAL>((Tendsto (fun n => ((↑e ∘ f) n).1) l (𝓝 (proj z)) ∧ Tendsto (fun n => ((↑e ∘ f) n).2) l (𝓝 (↑e z).2)) ∧ ∀ᶠ (a : α) in l, f a ∈ e.source) ↔ Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x => (↑e (f x)).2) l (𝓝 (↑e z).2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝¹ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>inst✝ : Unique I<GOAL>CompleteOrthogonalIdempotents e ↔ e default = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝¹ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>inst✝ : Unique I<GOAL>((∀ (i : I), IsIdempotentElem (e i)) ∧ ∀ (i j : I), i ≠ j → e i * e j = 0) ∧ ∑ i : I, e i = 1 ↔ e default = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝¹ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>inst✝ : Unique I<GOAL>e default = 1 → IsIdempotentElem (e default)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : LieRing L<VAR>inst✝⁹ : LieAlgebra R L<VAR>inst✝⁸ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>M₂ : Type u_5<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>χ : L → R<VAR>f : M →ₗ⁅R,L⁆ M₂<VAR>e : M ≃ₗ⁅R,L⁆ M₂<GOAL>LieSubmodule.map e.toLieModuleHom (weightSpace M χ) = weightSpace M₂ χ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>Q : AffineSubspace 𝕜 E<VAR>x : E<VAR>hx : x ∈ ↑Q<VAR>y : E<VAR>hy : y ∈ ↑Q<VAR>a b : 𝕜<VAR>x✝¹ : 0 ≤ a<VAR>x✝ : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ↑Q
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ : Set G<VAR>g : G<VAR>h : Gᵐᵒᵖ<VAR>s : Set G<GOAL>(fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ∣ b<GOAL>(b / a) ^ c = b ^ c / a ^ c
<VAR>a b d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ∣ b<GOAL>(b / a) ^ 0 = b ^ 0 / a ^ 0
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ∣ b<VAR>hc : c > 0<GOAL>(b / a) ^ c = b ^ c / a ^ c
<VAR>b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hc : c > 0<VAR>h : 0 ∣ b<GOAL>(b / 0) ^ c = b ^ c / 0 ^ c
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ∣ b<VAR>hc : c > 0<VAR>ha : a > 0<GOAL>(b / a) ^ c = b ^ c / a ^ c
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>h : a ∣ b<VAR>hc : c > 0<VAR>ha : a > 0<GOAL>b ^ c = a ^ c * (b / a) ^ c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>l : α → β<VAR>u : β → α<VAR>gc : GaloisConnection l u<VAR>f : (i : ι) → κ i → α<GOAL>l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<GOAL>Ici a * Ioi b ⊆ Ioi (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.12705) (N : Type ?u.12704) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Ici a * Ioi b ⊆ Ioi (a * b)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b : α<VAR>this : ∀ (M : Type ?u.12705) (N : Type ?u.12704) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : y ∈ Ici a<VAR>z : α<VAR>hzb : z ∈ Ioi b<GOAL>(fun x x_1 => x * x_1) y z ∈ Ioi (a * b)
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : A ⟶ K.X j<VAR>hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0<GOAL>(if hi : j = j then (singleObjXIsoOfEq c j A j hi).hom ≫ φ ≫ 𝟙 (K.X j) else 0) = (singleObjXSelf c j A).hom ≫ φ
<VAR>V : Type u<VAR>inst✝³ : Category.{v, u} V<VAR>inst✝² : HasZeroMorphisms V<VAR>inst✝¹ : HasZeroObject V<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex V c<VAR>j : ι<VAR>A : V<VAR>φ : A ⟶ K.X j<VAR>hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0<GOAL>(singleObjXIsoOfEq c j A j ⋯).hom ≫ φ = (singleObjXSelf c j A).hom ≫ φ
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : α<VAR>h : ∀ (ε : α), 1 < ε → a < b * ε<VAR>h₁ : b < a<GOAL>a < a
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>hJ : J.IsPrime<VAR>f : R →+* P<VAR>h : I.primeCompl ≤ Submonoid.comap f J.primeCompl<VAR>x : R<VAR>hx : x ∈ Ideal.comap f J<GOAL>x ∈ I
<VAR>R : Type u_1<VAR>inst✝³ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝² : CommSemiring S<VAR>inst✝¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝ : CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>hJ : J.IsPrime<VAR>f : R →+* P<VAR>h : I.primeCompl ≤ Submonoid.comap f J.primeCompl<VAR>x : R<VAR>hx : x ∉ I<GOAL>x ∉ Ideal.comap f J
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J K : FractionalIdeal S P<GOAL>I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J K : FractionalIdeal S P<GOAL>⟨↑I * ↑J, ⋯⟩ ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v v' w : U<VAR>p : Path u v<VAR>p' : Path u v'<VAR>e : v ⟶ w<VAR>e' : v' ⟶ w<VAR>h : p.cons e = p'.cons e'<GOAL>Hom.cast ⋯ ⋯ e = e'
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v v' w : U<VAR>p : Path u v<VAR>p' : Path u v'<VAR>e : v ⟶ w<VAR>e' : v' ⟶ w<VAR>h : p.cons e = p'.cons e'<GOAL>HEq e e'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>a < ↑⌊a⌋ + 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) → objs j ⟶ B<VAR>inst✝ : HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<VAR>j : J<GOAL>lift f fs w ≫ π arrows j = fs j
<VAR>A : Type u_1<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<GOAL>0 ≤ a ↔ IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal
<VAR>A : Type u_1<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<GOAL>IsSelfAdjoint a ∧ SpectrumRestricts a ⇑ContinuousMap.realToNNReal → 0 ≤ a
<VAR>A : Type u_1<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>a : A<VAR>ha₁ : IsSelfAdjoint a<VAR>ha₂ : SpectrumRestricts a ⇑ContinuousMap.realToNNReal<GOAL>0 ≤ a
<VAR>A : Type u_1<VAR>inst✝⁸ : Ring A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Algebra ℝ A<VAR>inst✝² : ContinuousFunctionalCalculus ℝ IsSelfAdjoint<VAR>inst✝¹ : NonnegSpectrumClass ℝ A<VAR>inst✝ : UniqueContinuousFunctionalCalculus ℝ A<VAR>x : A<VAR>hx : IsSelfAdjoint x<VAR>ha₁ : IsSelfAdjoint (x ^ 2)<VAR>ha₂ : SpectrumRestricts (x ^ 2) ⇑ContinuousMap.realToNNReal<GOAL>0 ≤ x ^ 2
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hz : z ≠ 0<GOAL>o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = ↑π
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>f.closure.inverse.graph = f.inverse.graph.topologicalClosure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>Submodule.map (LinearEquiv.prodComm R E F) f.graph.topologicalClosure = (Submodule.map (LinearEquiv.prodComm R E F) f.graph).topologicalClosure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>↑(Submodule.map (LinearEquiv.prodComm R E F) f.graph.topologicalClosure) = ↑(Submodule.map (LinearEquiv.prodComm R E F) f.graph).topologicalClosure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>(fun a => a.swap) '' _root_.closure ↑f.graph = _root_.closure ((fun a => a.swap) '' ↑f.graph)
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<GOAL>_root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<VAR>h1 : ⇑(LinearEquiv.prodComm R E F).toEquiv '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph<GOAL>_root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<VAR>h1 : ⇑(LinearEquiv.prodComm R E F).toEquiv '' ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' ↑f.graph<VAR>h2 : ⇑(LinearEquiv.prodComm R E F).toEquiv '' _root_.closure ↑f.graph = ⇑(LinearEquiv.prodComm R E F).toEquiv.symm ⁻¹' _root_.closure ↑f.graph<GOAL>_root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>hf : LinearMap.ker f.toFun = ⊥<VAR>hf' : f.IsClosable<VAR>hcf : LinearMap.ker f.closure.toFun = ⊥<VAR>h1 : (fun a => a.swap) '' ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' ↑f.graph<VAR>h2 : (fun a => a.swap) '' _root_.closure ↑f.graph = ⇑↑(LinearEquiv.prodComm R E F).symm ⁻¹' _root_.closure ↑f.graph<GOAL>_root_.closure (Prod.swap '' ↑f.graph) ⊆ Prod.swap '' _root_.closure ↑f.graph