ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>p : Submodule R M<VAR>hp : MapsTo ⇑f ↑p ↑p<VAR>hf : ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q<GOAL>∀ p_1 ≤ Submodule.comap (LinearMap.restrict f hp) p_1, ∃ q ≤ Submodule.comap (LinearMap.restrict f hp) q, IsCompl p_1 q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>p : Submodule R M<VAR>hp : MapsTo ⇑f ↑p ↑p<VAR>hf : ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q<VAR>q : Submodule R ↥p<VAR>hq : MapsTo ⇑f ↑(Submodule.map p.subtype q) ↑(Submodule.map p.subtype q)<VAR>r : Submodule R M<VAR>hr₁ : r ≤ Submodule.comap f r<VAR>hr₂ : IsCompl (Submodule.map p.subtype q) r<GOAL>IsCompl q (Submodule.comap p.subtype r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f g : End R M<VAR>p : Submodule R M<VAR>hp : MapsTo ⇑f ↑p ↑p<VAR>hf : ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q<VAR>q : Submodule R ↥p<VAR>hq : MapsTo ⇑f ↑(Submodule.map p.subtype q) ↑(Submodule.map p.subtype q)<VAR>r : Submodule R M<VAR>hr₁ : r ≤ Submodule.comap f r<VAR>hr₂ : IsCompl (Submodule.map p.subtype q) r<GOAL>IsCompl (Submodule.comap p.subtype (Submodule.map p.subtype q)) (Submodule.comap p.subtype r)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<GOAL>s = t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<VAR>f : ↑t ↪ ↑s := { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }<GOAL>s = t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<VAR>f : ↑t ↪ ↑s := { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }<VAR>h_surj : Surjective ⇑f<GOAL>s = t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<VAR>f : ↑t ↪ ↑s := { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }<VAR>h_surj : Surjective ⇑f<GOAL>s ⊆ t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y✝ : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<VAR>f : ↑t ↪ ↑s := { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }<VAR>h_surj : Surjective ⇑f<VAR>x : M<VAR>hx : x ∈ s<VAR>y : ↑t<VAR>hy : f y = ⟨x, hx⟩<GOAL>x ∈ t
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y✝ : M<VAR>inst✝ : Nontrivial R<VAR>s t : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<VAR>h : t ⊆ s<VAR>hst : s ⊆ ↑(span R t)<VAR>f : ↑t ↪ ↑s := { toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ }<VAR>h_surj : Surjective ⇑f<VAR>x : M<VAR>hx : x ∈ s<VAR>y : ↑t<VAR>hy : f y = ⟨x, hx⟩<GOAL>x = ↑y
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{?u.20097, u_1} D<VAR>P : MorphismProperty C<VAR>inst✝ : P.RespectsIso<GOAL>P.isoClosure = P
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M✝ : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>M : Sublattice β<VAR>e : β ≃o α<GOAL>map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M✝ : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>M : Sublattice β<VAR>e : β ≃o α<GOAL>↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L) = ↑M ↔ ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X✝ Y✝ : C<VAR>X Y : Cᵒᵖ<VAR>f : X ≅ Y<GOAL>f.hom.unop ≫ f.inv.unop = 𝟙 (Opposite.unop Y)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X✝ Y✝ : C<VAR>X Y : Cᵒᵖ<VAR>f : X ≅ Y<GOAL>f.inv.unop ≫ f.hom.unop = 𝟙 (Opposite.unop X)
<VAR>x y z : ℂ<VAR>h₁ : -π < (log x * y).im<VAR>h₂ : (log x * y).im ≤ π<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>x y z : ℂ<VAR>h₁ : -π < (log x * y).im<VAR>h₂ : (log x * y).im ≤ π<GOAL>(if x = 0 then if y * z = 0 then 1 else 0 else cexp (log x * (y * z))) = if (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 then if z = 0 then 1 else 0 else cexp (log (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) * z)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>s : Set P<VAR>inst✝ : FiniteDimensional k ↥(vectorSpan k s)<GOAL>Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>s : Set P<VAR>inst✝ : FiniteDimensional k ↥(vectorSpan k s)<VAR>h : Collinear k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 1<GOAL>Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : DivisionRing k<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AffineSpace V P<VAR>s : Set P<VAR>inst✝ : FiniteDimensional k ↥(vectorSpan k s)<VAR>h : Collinear k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 1<GOAL>Collinear k s ↔ finrank k ↥(vectorSpan k s) ≤ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>T1Space (SeparationQuotient X) ↔ R0Space X
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>(∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Symmetric Specializes
<VAR>n : ℕ<VAR>e : PartENat<GOAL>↑n.succ ≤ e ↔ ↑n < e
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>Z : ?m.78767<VAR>f : X → Y<GOAL>range (toPullbackDiag f) = pullbackDiagonal f
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>h : p.Monic<VAR>q : R[X]<GOAL>p * q = 0 ↔ q = 0
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hq : ¬IsUnit q<VAR>hsep : p.Separable<GOAL>multiplicity q p ≤ 1
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<GOAL>IsUnit q
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<GOAL>q * q ∣ p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<GOAL>q ^ 2 ∣ p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<GOAL>↑2 ≤ multiplicity q p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<VAR>h : { Dom := Part.Dom 1 ∧ Part.Dom 1, get := fun x => 2 } ≤ multiplicity q p<GOAL>↑2 ≤ multiplicity q p
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>p✝ q✝ : ℕ<VAR>p q : R[X]<VAR>hsep : p.Separable<VAR>hq : 1 < multiplicity q p<VAR>h : { Dom := Part.Dom 1, get := fun x => 2 } ≤ multiplicity q p<GOAL>↑2 ≤ multiplicity q p
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : ∀ (v w : V) (p q : G.Path v w), p = q<VAR>v : V<VAR>c : G.Walk v v<VAR>hc : c.IsCycle<GOAL>False
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>h : ∀ (v w : V) (p q : G.Path v w), p = q<VAR>v : V<VAR>c : G.Walk v v<VAR>hc : c.IsTrail ∧ ¬c = nil ∧ c.support.tail.Nodup<GOAL>False
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<VAR>a : A<VAR>ha : p a<GOAL>∃ φ, ClosedEmbedding ⇑φ ∧ φ (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a ∧ (∀ (f : C(↑(spectrum R a), R)), spectrum R (φ f) = range ⇑f) ∧ ∀ (f : C(↑(spectrum R a), R)), p (φ f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<VAR>a : A<VAR>ha : p a<GOAL>ClosedEmbedding ⇑(starAlgHom (cfcHom ⋯) ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<VAR>a : A<VAR>ha : p a<GOAL>(starAlgHom (cfcHom ⋯) ⋯) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<VAR>a : A<VAR>ha : p a<GOAL>∀ (f_1 : C(↑(spectrum R a), R)), spectrum R ((starAlgHom (cfcHom ⋯) ⋯) f_1) = range ⇑f_1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>f : C(S, R)<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h0 : p 0<VAR>h : ∀ (a : A), p a ↔ q a ∧ SpectrumRestricts a ⇑f<VAR>h_cpct : ∀ (a : A), q a → CompactSpace ↑(spectrum S a)<VAR>a : A<VAR>ha : p a<GOAL>∀ (f_1 : C(↑(spectrum R a), R)), p ((starAlgHom (cfcHom ⋯) ⋯) f_1)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>l : Filter α<VAR>m : Filter β<VAR>p : α × β → Prop<GOAL>(∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>x y : L<GOAL>(∃ k, (((ad R L) x - 0 • 1) ^ k) y = 0) ↔ ∃ n, ((ad R L) x ^ n) y = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>inst✝ : Nonempty α<VAR>h_Union : ⋃ i, s i = univ<GOAL>(⋃ i, s i).Nonempty
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>e : ↑(F.obj (X ⨿ Y)) ≃ ↑(F.obj X) ⊕ ↑(F.obj Y) := ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫ Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv<GOAL>Nat.card ↑(F.obj (X ⨿ Y)) = Nat.card ↑(F.obj X) + Nat.card ↑(F.obj Y)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : PreGaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X Y : C<VAR>e : ↑(F.obj (X ⨿ Y)) ≃ ↑(F.obj X) ⊕ ↑(F.obj Y) := ((PreservesColimitPair.iso (F ⋙ FintypeCat.incl) X Y).symm ≪≫ Types.binaryCoproductIso (FintypeCat.incl.obj (F.obj X)) (FintypeCat.incl.obj (F.obj Y))).toEquiv<GOAL>Nat.card ↑(F.obj (X ⨿ Y)) = Nat.card (↑(F.obj X) ⊕ ↑(F.obj Y))
<VAR>f : Char → Char<VAR>s : String<GOAL>map f s = { data := List.map f s.data }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>ρ : Measure (α × ℝ)<VAR>r : ℝ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(ρ.IicSnd r) s = ρ (s ×ˢ Iic r)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y'✝ : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p'✝ : Y✝ ⟶ Y'✝<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : Arrow.mk p ≅ Arrow.mk p'<VAR>a✝ : HasLiftingProperty i p<GOAL>HasLiftingProperty i p'
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>A✝ B✝ B' X✝ Y✝ Y'✝ : C<VAR>i✝ : A✝ ⟶ B✝<VAR>i' : B✝ ⟶ B'<VAR>p✝ : X✝ ⟶ Y✝<VAR>p'✝ : Y✝ ⟶ Y'✝<VAR>A B X Y X' Y' : C<VAR>i : A ⟶ B<VAR>p : X ⟶ Y<VAR>p' : X' ⟶ Y'<VAR>e : Arrow.mk p ≅ Arrow.mk p'<VAR>a✝ : HasLiftingProperty i p'<GOAL>HasLiftingProperty i p
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝⁵ : DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>inst✝⁴ : (a : α) → Zero (N a)<VAR>inst✝³ : (a : α) → Zero (M a)<VAR>inst✝² : (a : α) → Zero (P a)<VAR>inst✝¹ : (a : α) → DecidableEq (M a)<VAR>inst✝ : (a : α) → DecidableEq (P a)<VAR>F : (a : α) → M a → N a → P a<VAR>F0 : ∀ (a : α), F a 0 0 = 0<VAR>f₁ f₂ : Π₀ (a : α), M a<VAR>g : Π₀ (a : α), N a<VAR>hF : ∀ (a : α) (g : N a), Function.Injective fun f => F a f g<VAR>a : α<GOAL>a ∈ (zipWith F F0 f₁ g).neLocus (zipWith F F0 f₂ g) ↔ a ∈ f₁.neLocus f₂
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime x (y * z)<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x y z : α<VAR>H : IsRelPrime (y * z) x<GOAL>IsRelPrime y x
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card G<VAR>a : G<VAR>ha : ∀ (x : G), x ∈ zpowers a<GOAL>∃ a, a ^ k ≠ 1
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>k_lt_card_G : k < Fintype.card G<VAR>a : G<VAR>ha : ∀ (x : G), x ∈ zpowers a<GOAL>a ^ k ≠ 1
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>a : G<VAR>ha : ∀ (x : G), x ∈ zpowers a<VAR>k_lt_card_G : a ^ k = 1<GOAL>Fintype.card G ≤ k
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>a : G<VAR>ha : ∀ (x : G), x ∈ zpowers a<VAR>k_lt_card_G : a ^ k = 1<GOAL>Fintype.card G = orderOf a
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝² : Group α<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fintype G<VAR>k : ℕ<VAR>k_pos : k ≠ 0<VAR>a : G<VAR>ha : ∀ (x : G), x ∈ zpowers a<VAR>k_lt_card_G : a ^ k = 1<GOAL>⊤ ≤ zpowers a
<VAR>R : Type u_1<VAR>inst✝²⁰ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁹ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁸ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹⁷ : AddCommMonoid M<VAR>inst✝¹⁶ : AddCommMonoid N<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : AddCommMonoid Q<VAR>inst✝¹³ : AddCommMonoid S<VAR>inst✝¹² : AddCommMonoid T<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module R N<VAR>inst✝⁹ : Module R P<VAR>inst✝⁸ : Module R Q<VAR>inst✝⁷ : Module R S<VAR>inst✝⁶ : Module R T<VAR>inst✝⁵ : DistribMulAction R' M<VAR>inst✝⁴ : Module R'' M<VAR>P' : Type u_10<VAR>Q' : Type u_11<VAR>inst✝³ : AddCommMonoid P'<VAR>inst✝² : Module R P'<VAR>inst✝¹ : AddCommMonoid Q'<VAR>inst✝ : Module R Q'<VAR>f : M →ₗ[R] P<VAR>g₁ g₂ : N →ₗ[R] Q<VAR>x✝¹ : M<VAR>x✝ : N<GOAL>(((mk R M N).compr₂ (map f (g₁ + g₂))) x✝¹) x✝ = (((mk R M N).compr₂ (map f g₁ + map f g₂)) x✝¹) x✝
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t))) ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)<GOAL>HasSum (fun n => s.Gammaℝ / ↑|↑n + a| ^ s / 2) (mellin (fun t => (↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2) (s / 2))
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t))) ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)<GOAL>Summable fun i => ‖1 / 2‖ / |↑i + a| ^ s.re
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t))) ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)<VAR>n : ℤ<GOAL>s.Gammaℝ / ↑|↑n + a| ^ s / 2 = s.Gammaℝ * (1 / 2) / ↑|↑n + a| ^ s
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ i₁' : I₁<VAR>h : c₁.Rel i₁ i₁'<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_5, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<VAR>i₁₂ : I₁₂<VAR>h : c₁.Rel i₁ (c₁.next i₁)<GOAL>K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>S : Set α<VAR>hg : UniformInducing g<GOAL>map (fun x => (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 α ⊓ 𝓟 (S ×ˢ S)) ≤ 𝓤 γ
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<VAR>ht₀ : t.Nonempty<VAR>ht₁ : BddBelow t<GOAL>sSup (s / t) = sSup s / sInf t
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<VAR>x : R<GOAL>x ∈ ↑⊥ ↔ x = 0
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (t * s)
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t : Set G<VAR>ht : IsClosed t<VAR>hs : IsCompact s<GOAL>IsClosed (op '' s • t)