ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hf : u = fun i => g.symm (g (u i))<GOAL>g.symm (limsup (fun x => g (u x)) f) ≤ limsup (fun i => g.symm (g (u i))) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hf : u = fun i => g.symm (g (u i))<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g.symm (g (u x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>γ : Type u_6<VAR>inst✝¹ : ConditionallyCompleteLattice β<VAR>inst✝ : ConditionallyCompleteLattice γ<VAR>f : Filter α<VAR>u : α → β<VAR>g : β ≃o γ<VAR>hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => g (u x)) _auto✝<VAR>hf : u = fun i => g.symm (g (u i))<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => u x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>l : Filter α<VAR>s : Set α<VAR>x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s<VAR>_t : Set α<VAR>htf : {s | #↑s < c} _t<VAR>hts : _tᶜ ⊆ s<GOAL>s ∈ cocardinal α hreg
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>hreg : c.IsRegular<VAR>l : Filter α<VAR>s : Set α<VAR>x✝ : ∃ i, {s | #↑s < c} i ∧ iᶜ ⊆ s<VAR>_t : Set α<VAR>htf : {s | #↑s < c} _t<VAR>hts : _tᶜ ⊆ s<VAR>this : #↑sᶜ < c<GOAL>s ∈ cocardinal α hreg
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : Fintype I<VAR>inst✝² : Fintype J<VAR>inst✝¹ : DecidableEq I<VAR>inst✝ : DecidableEq J<VAR>x✝¹ x✝ : Matrix I I (Matrix J J R)<VAR>i✝ j✝ : I × J<GOAL>__spread✝⁻⁰.toFun (x✝¹ * x✝) i✝ j✝ = (__spread✝⁻⁰.toFun x✝¹ * __spread✝⁻⁰.toFun x✝) i✝ j✝
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>a : ↥S.leftInv<VAR>b : M<GOAL>↑(S.fromLeftInv a) = b ↔ ↑a * b = 1
<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<GOAL>‖0‖₊ = 0
<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<GOAL>(eLpNorm (↑↑0) p μ).toNNReal = 0
<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<GOAL>(eLpNorm (↑0) p μ).toNNReal = 0
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X✝ Y✝ Z✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>H : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T), Q (g.comp f) → Q g<VAR>Z : Scheme<VAR>hZ : IsAffine Z<VAR>Y : Scheme<VAR>g : Y ⟶ Z<VAR>hY✝ : IsAffine Y<VAR>X : Scheme<VAR>f : X ⟶ Y<VAR>h : P (f ≫ g)<VAR>hY : IsAffine X<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X✝ Y✝ Z✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>g✝ : Y✝ ⟶ Z✝<VAR>H : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T), Q (g.comp f) → Q g<VAR>Z : Scheme<VAR>hZ : IsAffine Z<VAR>Y : Scheme<VAR>g : Y ⟶ Z<VAR>hY✝ : IsAffine Y<VAR>X : Scheme<VAR>f : X ⟶ Y<VAR>h : Q (Scheme.Hom.app (f ≫ g) ⊤)<VAR>hY : IsAffine X<GOAL>Q (Scheme.Hom.app f ⊤)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>p : ι → Prop<VAR>s : X → ι → Set X<VAR>h : ∀ (x : X), (𝓝 x).HasBasis p (s x)<VAR>h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)<VAR>x : X<GOAL>(𝓝 x).HasBasis (fun s => s ∈ 𝓝 x ∧ IsPathConnected s) id
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>p : ι → Prop<VAR>s : X → ι → Set X<VAR>h : ∀ (x : X), (𝓝 x).HasBasis p (s x)<VAR>h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)<VAR>x : X<GOAL>∀ (i : ι), p i → ∃ i', (i' ∈ 𝓝 x ∧ IsPathConnected i') ∧ id i' ⊆ s x i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x✝ y z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>p : ι → Prop<VAR>s : X → ι → Set X<VAR>h : ∀ (x : X), (𝓝 x).HasBasis p (s x)<VAR>h' : ∀ (x : X) (i : ι), p i → IsPathConnected (s x i)<VAR>x : X<GOAL>∀ (i' : Set X), i' ∈ 𝓝 x ∧ IsPathConnected i' → ∃ i, p i ∧ s x i ⊆ id i'
<VAR>a : ℤ<VAR>b : ℕ<GOAL>{0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom)
<VAR>a : ℤ<VAR>b : ℕ<GOAL>{0, -1, 1} = ↑(MonoidHom.mrange ↑SignType.castHom)
<VAR>a : ℤ<VAR>b : ℕ<VAR>x✝ : ℤ<VAR>ha' : x✝ ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯<GOAL>x✝ ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
<VAR>a : ℤ<VAR>b p : ℕ<VAR>hp : p ∈ b.primeFactorsList<VAR>ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯<GOAL>legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
<VAR>a : ℤ<VAR>b p : ℕ<VAR>hp : p ∈ b.primeFactorsList<VAR>ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯<VAR>this : Fact (Nat.Prime p)<GOAL>legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>h : i ≠ j<VAR>a b c d : ↑(Ω^ N X x)<VAR>y✝ : N → ↑I<GOAL>(transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i j : N<VAR>h : i ≠ j<VAR>a b c d : ↑(Ω^ N X x)<VAR>y✝ : N → ↑I<GOAL>(if ↑(y✝ i) ≤ 1 / 2 then if ↑(y✝ j) ≤ 1 / 2 then a (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) else b (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) else if ↑(y✝ j) ≤ 1 / 2 then c (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) else d (Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1)))) = if ↑(y✝ j) ≤ 1 / 2 then if ↑(y✝ i) ≤ 1 / 2 then a (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) else c (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j)))) i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1))) else if ↑(y✝ i) ≤ 1 / 2 then b (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i)))) else d (Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ j) - 1))) i (Set.projIcc 0 1 transAt.proof_2 (2 * ↑(y✝ i) - 1)))
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a * b / c = a / c * b
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>adjoin R s ≤ S ↔ s ≤ ↑S
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<VAR>S : NonUnitalStarSubalgebra R A<GOAL>s ∪ star s ⊆ ↑S ↔ s ≤ ↑S
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁵ : GroupWithZero G₀<VAR>inst✝⁴ : Bornology G₀<VAR>inst✝³ : MulAction G₀ α<VAR>s✝ t u : Set α<VAR>S : Set (Set α)<VAR>inst✝² : (cobounded G₀).NeBot<VAR>E : Type u_3<VAR>inst✝¹ : AddMonoid E<VAR>inst✝ : DistribMulAction G₀ E<VAR>s : Set E<GOAL>Absorbs G₀ s 0 ↔ 0 ∈ s
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F₁ F₂ F₃ : Sheaf J A<VAR>φ : F₁ ⟶ F₂<VAR>ψ : F₂ ⟶ F₃<GOAL>Presheaf.IsLocallySurjective J ((sheafToPresheaf J A).map φ) ↔ IsLocallySurjective φ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>h : IsUnit p<VAR>a✝ : Nontrivial R<GOAL>p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q✝ : R[X]<VAR>h : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>hq : p * q = 1<GOAL>p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q✝ : R[X]<VAR>h : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>hq : p * q = 1<VAR>this : (p * q).natDegree = p.natDegree + q.natDegree<GOAL>p.natDegree = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q✝ : R[X]<VAR>h : IsUnit p<VAR>a✝ : Nontrivial R<VAR>q : R[X]<VAR>hq : p * q = 1<VAR>this : p.natDegree = 0 ∧ q.natDegree = 0<GOAL>p.natDegree = 0
<VAR>C D : Type u₁<VAR>inst✝⁹ : SmallCategory C<VAR>inst✝⁸ : SmallCategory D<VAR>E : Type u₂<VAR>inst✝⁷ : Category.{u₁, u₂} E<VAR>inst✝⁶ : ConcreteCategory E<VAR>inst✝⁵ : HasLimits E<VAR>inst✝⁴ : HasColimits E<VAR>inst✝³ : ReflectsLimits (forget E)<VAR>inst✝² : PreservesFilteredColimits (forget E)<VAR>inst✝¹ : PreservesLimits (forget E)<VAR>inst✝ : HasFiniteLimits C<VAR>F : C ⥤ D<VAR>H : RepresentablyFlat F.op.lan<VAR>this✝ : PreservesFiniteLimits F.op.lan<VAR>this : PreservesFiniteLimits F<GOAL>RepresentablyFlat F
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>h : IsUnit a<VAR>a✝ : Nontrivial A<GOAL>IsUnit ⟨a, ⋯⟩
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>h : IsUnit a<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<GOAL>IsUnit a'
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>h : IsUnit a<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<GOAL>IsUnit (star a' * a')
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<VAR>h : IsUnit (star a * a)<GOAL>IsUnit (star a' * a')
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<VAR>h : IsUnit (star a * a)<VAR>h₁ : ↑‖star a * a‖ ≠ 0<GOAL>IsUnit (star a' * a')
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<VAR>h : IsUnit (star a * a)<VAR>h₁ : ↑‖star a * a‖ ≠ 0<VAR>u : (↥(elementalStarAlgebra ℂ a))ˣ := (Units.map ↑(algebraMap ℂ ↥(elementalStarAlgebra ℂ a))) (Units.mk0 (↑‖star a * a‖) h₁)<GOAL>‖star a' * a' - ↑u‖ < ‖↑u⁻¹‖⁻¹
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<VAR>h : IsUnit (star a * a)<VAR>h₁ : ↑‖star a * a‖ ≠ 0<VAR>u : (↥(elementalStarAlgebra ℂ a))ˣ := (Units.map ↑(algebraMap ℂ ↥(elementalStarAlgebra ℂ a))) (Units.mk0 (↑‖star a * a‖) h₁)<GOAL>‖star a' * a' - (algebraMap ℂ ↥(elementalStarAlgebra ℂ a)) ↑‖star a * a‖‖ < ‖star a * a‖
<VAR>A : Type u_1<VAR>inst✝⁶ : NormedRing A<VAR>inst✝⁵ : NormedAlgebra ℂ A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : CompleteSpace A<VAR>a : A<VAR>inst✝ : IsStarNormal a<VAR>S : StarSubalgebra ℂ A<VAR>a✝ : Nontrivial A<VAR>a' : ↥(elementalStarAlgebra ℂ a) := ⟨a, ⋯⟩<VAR>h : IsUnit (star a * a)<VAR>h₁ : ↑‖star a * a‖ ≠ 0<VAR>u : (↥(elementalStarAlgebra ℂ a))ˣ := (Units.map ↑(algebraMap ℂ ↥(elementalStarAlgebra ℂ a))) (Units.mk0 (↑‖star a * a‖) h₁)<VAR>h₂ : ∀ z ∈ spectrum ℂ ((algebraMap ℂ A) ↑‖star a * a‖ - star a * a), ‖z‖₊ < ‖star a * a‖₊<GOAL>‖star a' * a' - (algebraMap ℂ ↥(elementalStarAlgebra ℂ a)) ↑‖star a * a‖‖ < ‖star a * a‖
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set Aᵐᵒᵖ<GOAL>(Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s)
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set Aᵐᵒᵖ<GOAL>(Algebra.adjoin R s).unop.toSubsemiring = (Algebra.adjoin R (MulOpposite.op ⁻¹' s)).toSubsemiring
<VAR>ι : Sort u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>s : Set Aᵐᵒᵖ<GOAL>Subsemiring.closure (MulOpposite.op ⁻¹' Set.range ⇑(algebraMap R Aᵐᵒᵖ) ∪ MulOpposite.op ⁻¹' s) = Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ MulOpposite.op ⁻¹' s)
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<VAR>F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<VAR>F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }<VAR>this : Summable (fourierCoeff ⇑F)<GOAL>∑' (n : ℤ), f (x + ↑n) = ∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<VAR>F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }<VAR>this : Summable (fourierCoeff ⇑F)<GOAL>∑' (n : ℤ), f (x + ↑n) = F ↑x
<VAR>f : C(ℝ, ℂ)<VAR>h_norm : ∀ (K : Compacts ℝ), Summable fun n => ‖ContinuousMap.restrict (↑K) (f.comp (ContinuousMap.addRight ↑n))‖<VAR>h_sum : Summable fun n => 𝓕 ⇑f ↑n<VAR>x : ℝ<VAR>F : C(UnitAddCircle, ℂ) := { toFun := ⋯.lift, continuous_toFun := ⋯ }<VAR>this : Summable (fourierCoeff ⇑F)<GOAL>∑' (n : ℤ), 𝓕 ⇑f ↑n * (fourier n) ↑x = ∑' (b : ℤ), fourierCoeff (⇑F) b • (fourier b) ↑x
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<GOAL>(algebraMap (RatFunc F) (LaurentSeries F)) ((algebraMap F[X] (RatFunc F)) p / (algebraMap F[X] (RatFunc F)) q) = (algebraMap F[X] (LaurentSeries F)) p / (algebraMap F[X] (LaurentSeries F)) q
<VAR>F : Type u_1<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module ℝ F<VAR>inst✝³ : TopologicalSpace F<VAR>E : Type u_2<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : TopologicalSpace E<VAR>s : Set F<VAR>h : AmpleSet s<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L ⁻¹' s)
<VAR>F : Type u_1<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module ℝ F<VAR>inst✝³ : TopologicalSpace F<VAR>E : Type u_2<VAR>inst✝² : AddCommGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : TopologicalSpace E<VAR>s : Set F<VAR>h : AmpleSet s<VAR>L : E ≃ᵃL[ℝ] F<GOAL>AmpleSet (⇑L.symm '' s)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>b b' x : F<GOAL>(tangentBundleCore 𝓘(𝕜, F) F).coordChange (achart F b) (achart F b') x = 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : BooleanAlgebra α<GOAL>Disjoint x yᶜ ↔ x ≤ y
<VAR>α : Type u_1<VAR>F : Type u_2<VAR>F' : Type u_3<VAR>𝕜 : Type u_4<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup F'<VAR>inst✝² : NormedSpace 𝕜 F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → F'<VAR>s : Set α<VAR>h : f =ᶠ[ae μ] g<VAR>hm : m ≤ m0<VAR>hμm this : SigmaFinite (μ.trim hm)<GOAL>μ[f|m] =ᶠ[ae μ] μ[g|m]
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a b c : α<VAR>inst✝ : DecidableEq α<VAR>h : a ≤ b<GOAL>Icc a b \ Ioo a b = {a, b}
<VAR>m n a b c d : ℕ<GOAL>a ≡ b [MOD 0] ↔ a = b
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y ⊓ (x ⊔ z) ⊔ y \ x ⊓ y \ z = (y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ (x ⊔ z) ⊔ y \ x) ⊓ (y ⊓ (x ⊔ z) ⊔ y \ z) = (y ⊓ x ⊔ y ⊓ z ⊔ y \ x) ⊓ (y ⊓ x ⊔ y ⊓ z ⊔ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ z ⊔ (y ⊓ x ⊔ y \ x)) ⊓ (y ⊓ x ⊔ (y ⊓ z ⊔ y \ z)) = (y ⊓ z ⊔ y) ⊓ (y ⊓ x ⊔ y)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊔ y ⊓ z) ⊓ (y ⊔ y ⊓ x) = y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y ⊓ (x ⊔ z) ⊓ (y \ x ⊓ y \ z) = (y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>(y ⊓ x ⊔ y ⊓ z) ⊓ (y \ x ⊓ y \ z) = y ⊓ x ⊓ (y \ x ⊓ y \ z) ⊔ y ⊓ z ⊓ (y \ x ⊓ y \ z)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y ⊓ x ⊓ y \ x ⊓ y \ z ⊔ y \ x ⊓ (y \ z ⊓ (y ⊓ z)) = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>s✝ t s : Finset α<GOAL>filter (fun x => x ∈ s) univ = s
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K 0<VAR>m₁ : ℤ<VAR>h₁ : n₁ + 1 = m₁<GOAL>δ n₁ m₁ (z₁.comp z₂ ⋯) = z₁.comp (δ 0 1 z₂) h₁ + (δ n₁ m₁ z₁).comp z₂ ⋯
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<GOAL>hausdorffDist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<VAR>hs : s = ∅<GOAL>hausdorffDist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<VAR>hs : s.Nonempty<GOAL>hausdorffDist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<VAR>hs : s.Nonempty<VAR>ht : t = ∅<GOAL>hausdorffDist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>H1 : ∀ x ∈ s, infDist x t ≤ r<VAR>H2 : ∀ x ∈ t, infDist x s ≤ r<VAR>h1 : ¬hausdorffEdist s t = ⊤<VAR>hs : s.Nonempty<VAR>ht : t.Nonempty<GOAL>hausdorffDist s t ≤ r