ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hs : s ⊆ e.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I).symm ⁻¹' s ∩ range ↑I) (↑(e.extend I) x) ↔ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>he : e ∈ maximalAtlas I M<VAR>hs : s ⊆ e.source<VAR>x : M<VAR>hx : x ∈ s<GOAL>𝓝[↑(e.extend I).symm ⁻¹' s ∩ range ↑I] ↑(e.extend I) x = 𝓝[↑(e.extend I) '' s] ↑(e.extend I) x
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>(↑((Types.limitEquivSections (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂})) ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫ ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))) A).down = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>(limit.π (incl F ⋙ (F ⋙ FintypeCat.incl) ⋙ uliftFunctor.{u₁, u₂}) A ((colimitCoyonedaHomIsoLimit' (incl F) (F ⋙ FintypeCat.incl)).hom ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom ≫ ((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f))).down = f.app A.obj A.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>f : End F<VAR>A : PointedGaloisObject F<GOAL>(((FullyFaithful.ofFullyFaithful FintypeCat.incl).whiskeringRight C).homEquiv f).app A.obj ((colimit.isoColimitCocone { cocone := cocone F, isColimit := isColimit F }).hom.app A.obj ((colimit.ι ((incl F).op ⋙ coyoneda) (Opposite.op A)).app A.obj (𝟙 A.obj))) = f.app A.obj A.pt
<VAR>x y : ZFSet<GOAL>x.toSet ⊆ y.toSet ↔ x ⊆ y
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>A.adjugate i j = (A.updateRow j (Pi.single i 1)).det
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<GOAL>U R (-2) = -1
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f'✝ : α → β → γ<VAR>g✝ g'✝ : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>g : γ → δ<VAR>f' : β → α' → δ<VAR>g' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)<GOAL>g '' image2 f ↑s ↑t = image2 f' (↑t) (g' '' ↑s)
<VAR>θ ψ : Angle<VAR>h : 2 • θ + 2 • ψ = ↑π<GOAL>|θ.cos| = |ψ.sin|
<VAR>θ ψ : Angle<VAR>h : θ = ↑(π / 2) - ψ ∨ θ = ↑(π / 2) - ψ + ↑π<GOAL>|θ.cos| = |ψ.sin|
<VAR>y : ℝ<VAR>h : y < 0<GOAL>⊤ ^ y = 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>f : ι → κ<VAR>s : Finset κ<VAR>hf : Set.InjOn f (f ⁻¹' ↑s)<VAR>g : κ → β<VAR>hg : ∀ x ∈ s, x ∉ Set.range f → g x = 1<GOAL>∏ x ∈ s.preimage f hf, g (f x) = ∏ x ∈ s, g x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>IsCompact s ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>Monotone fun f => ∃ x ∈ s, ClusterPt x f
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>(∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x ↑f) ↔ ∀ (f : Ultrafilter X), ↑f ≤ 𝓟 s → ∃ x ∈ s, ↑f ≤ 𝓝 x
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : z ≤ b<GOAL>(z - 1).inductionOn' b H0 Hs Hp = Hp z hz (z.inductionOn' b H0 Hs Hp)
<VAR>a b✝ c d m n : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : z ≤ b<GOAL>HEq (match z - 1 - b with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n) (Hp z hz (z.inductionOn' b H0 Hs Hp))
<VAR>a b✝ c d m n✝ : ℤ<VAR>C : ℤ → Sort u_1<VAR>z b : ℤ<VAR>H0 : C b<VAR>Hs : (k : ℤ) → b ≤ k → C k → C (k + 1)<VAR>Hp : (k : ℤ) → k ≤ b → C k → C (k - 1)<VAR>hz : z ≤ b<VAR>n : ℕ<VAR>hn : z - 1 - b = -[n+1]<GOAL>HEq (match z - 1 - b with | ofNat n => inductionOn'.pos b H0 Hs n | -[n+1] => inductionOn'.neg b H0 Hp n) (Hp z hz (z.inductionOn' b H0 Hs Hp))
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>w : α → ℝ≥0<VAR>wpos : ∀ (x : α), 0 < w x<VAR>wmeas : Measurable w<VAR>wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>w : α → ℝ≥0<VAR>wpos : ∀ (x : α), 0 < w x<VAR>wmeas : Measurable w<VAR>wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2<VAR>f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : μ.WeaklyRegular<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>fmeas : Measurable f<VAR>ε : ℝ≥0∞<VAR>ε0 : ε ≠ 0<VAR>this : ε / 2 ≠ 0<VAR>w : α → ℝ≥0<VAR>wpos : ∀ (x : α), 0 < w x<VAR>wmeas : Measurable w<VAR>wint : ∫⁻ (x : α), ↑(w x) ∂μ < ε / 2<VAR>f' : α → ℝ≥0∞ := fun x => ↑(f x + w x)<VAR>g : α → ℝ≥0∞<VAR>le_g : ∀ (x : α), f' x ≤ g x<VAR>gcont : LowerSemicontinuous g<VAR>gint : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f' x ∂μ + ε / 2<GOAL>∃ g, (∀ (x : α), ↑(f x) < g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), ↑(f x) ∂μ + ε
<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✝ : Mul P<VAR>c✝ : Con M<VAR>r : M → M → Prop<VAR>c : Con M<VAR>h : ∀ (x y : M), r x y → c x y<GOAL>conGen r ≤ c
<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✝ : Mul P<VAR>c✝ : Con M<VAR>r : M → M → Prop<VAR>c : Con M<VAR>h : ∀ (x y : M), r x y → c x y<GOAL>sInf {s | ∀ (x y : M), r x y → s x y} ≤ c
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>eX eX' : PartialHomeomorph X X'<VAR>eY eY' : PartialHomeomorph Y Y'<VAR>h : (eX'.prod eY').source.Nonempty<GOAL>eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f g✝ : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<VAR>inst✝ : DecidableEq γ<VAR>g : β → γ<GOAL>(image g (image f s)).val = (image (g ∘ f) s).val
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>hr : o < type r<GOAL>type s = type r
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : IsWellOrder β s<VAR>f : r ≃r s<VAR>o : Ordinal.{u}<VAR>hr : o < type r<GOAL>{ α := β, r := s, wo := inst✝ } ≈ { α := α, r := r, wo := inst✝¹ }
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : DecidableEq α<VAR>s : Finset γ<VAR>t : γ → Finset α<VAR>hs : (↑s).PairwiseDisjoint t<GOAL>∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<GOAL>IsField R
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this : Nontrivial S<GOAL>IsField R
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝ : Nontrivial S<VAR>this : Nontrivial R<GOAL>IsField R
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝ : Nontrivial S<VAR>this : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<GOAL>∃ b, a * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝ : Nontrivial S<VAR>this : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<VAR>a_inv : S<VAR>ha_inv : (algebraMap R S) a * a_inv = 1<GOAL>∃ b, a * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝¹ : Nontrivial S<VAR>this✝ : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<VAR>a_inv : S<VAR>ha_inv : (algebraMap R S) a * a_inv = 1<VAR>this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible<GOAL>∃ b, a * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝¹ : Nontrivial S<VAR>this✝ : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<VAR>a_inv : S<VAR>ha_inv : (algebraMap R S) a * a_inv = 1<VAR>this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R S) a_inv p = 0<GOAL>∃ b, a * b = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝¹ : Nontrivial S<VAR>this✝ : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<VAR>a_inv : S<VAR>ha_inv : (algebraMap R S) a * a_inv = 1<VAR>this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R S) a_inv p = 0<GOAL>a * -eval a p.reverse.divX = 1
<VAR>R✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S✝ : Type u_4<VAR>T : Type u_5<VAR>inst✝¹² : CommRing R✝<VAR>inst✝¹¹ : CommRing A<VAR>inst✝¹⁰ : Ring B<VAR>inst✝⁹ : CommRing S✝<VAR>inst✝⁸ : CommRing T<VAR>inst✝⁷ : Algebra A B<VAR>inst✝⁶ : Algebra R✝ B<VAR>f : R✝ →+* S✝<VAR>g : S✝ →+* T<VAR>inst✝⁵ : Algebra R✝ A<VAR>inst✝⁴ : IsScalarTower R✝ A B<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra.IsIntegral R S<VAR>hRS : Function.Injective ⇑(algebraMap R S)<VAR>hS : IsField S<VAR>this✝¹ : Nontrivial S<VAR>this✝ : Nontrivial R<VAR>a : R<VAR>ha : a ≠ 0<VAR>a_inv : S<VAR>ha_inv : (algebraMap R S) a * a_inv = 1<VAR>this : Invertible a_inv := (Units.mkOfMulEqOne a_inv ((algebraMap R S) a) ⋯).invertible<VAR>p : R[X]<VAR>p_monic : p.Monic<VAR>hp : eval₂ (algebraMap R S) a_inv p = 0<GOAL>(aeval ((algebraMap R S) a)) p.reverse = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>(a + b) / c = a / c + b / c
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.51659, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>X₂ : D₂<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.51659, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>X₂ : D₂<VAR>this : L₂.EssSurj<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>D₂ : Type u_3<VAR>H : Type u_4<VAR>inst✝⁵ : Category.{u_5, u_1} C₁<VAR>inst✝⁴ : Category.{u_6, u_2} C₂<VAR>inst✝³ : Category.{u_7, u_3} D₂<VAR>inst✝² : Category.{?u.51659, u_4} H<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>inst✝ : Φ.HasRightResolutions<VAR>X₂ : D₂<VAR>this : L₂.EssSurj<VAR>R : Φ.RightResolution (L₂.objPreimage X₂)<GOAL>X₂ ∈ (Φ.functor ⋙ L₂).essImage
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>r : ℕ<VAR>A : Finset α<GOAL>A ∈ 𝒜 → A ∈ powersetCard r univ ↔ A ∈ ↑𝒜 → A.card = r
<VAR>cs₁ cs₂ : List Char<GOAL>utf8Len (cs₁.reverseAux cs₂) = utf8Len cs₁ + utf8Len cs₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>t : Set E<VAR>x y : E<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>hs₁ : Convex ℝ ∅<VAR>hs₂ : IsOpen ∅<VAR>disj : Disjoint ∅ t<GOAL>∃ f u, (∀ a ∈ ∅, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>ht₁ : Convex ℝ ∅<VAR>ht₃ : IsOpen ∅<VAR>disj : Disjoint s ∅<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ ∅, u < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : TopologicalAddGroup E<VAR>inst✝¹ : Module ℝ E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s t<VAR>a₀ : E<VAR>ha₀ : a₀ ∈ s<VAR>b₀ : E<VAR>hb₀ : b₀ ∈ t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b