ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>z : G<GOAL>‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra L A<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower K L A<VAR>L_alg : Algebra.IsAlgebraic K L<VAR>A_alg : Algebra.IsAlgebraic L A<GOAL>Algebra.IsAlgebraic K A
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra L A<VAR>inst✝¹ : Algebra K A<VAR>inst✝ : IsScalarTower K L A<VAR>L_alg : Algebra.IsIntegral K L<VAR>A_alg : Algebra.IsIntegral L A<GOAL>Algebra.IsIntegral K A
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧ |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2<VAR>H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2<GOAL>abs' (↑(f - CauSeq.const (⇑abs') (limAux f)) j) < ε
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2 ∧ |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : |↑(⟨fun n => (↑f n).re, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩)) j| < ε / 2<VAR>H₂ : |↑(⟨fun n => (↑f n).im, ⋯⟩ - CauSeq.const _root_.abs (CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩)) j| < ε / 2<GOAL>|(↑(f - CauSeq.const (⇑abs') (limAux f)) j).re| + |(↑(f - CauSeq.const (⇑abs') (limAux f)) j).im| < ε
<VAR>f : CauSeq ℂ ⇑abs'<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>i : ℕ<VAR>H : ∀ j ≥ i, |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2 ∧ |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2<VAR>j : ℕ<VAR>ij : j ≥ i<VAR>H₁ : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| < ε / 2<VAR>H₂ : |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2<VAR>this : |(↑f j).re - CauSeq.lim ⟨fun n => (↑f n).re, ⋯⟩| + |(↑f j).im - CauSeq.lim ⟨fun n => (↑f n).im, ⋯⟩| < ε / 2 + ε / 2<GOAL>|(↑f j).re - (cauSeqRe f).lim| + |(↑f j).im - (cauSeqIm f).lim| < ε
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑p + 1 + ↑p + 1 = ↑p + ↑p + 1 + 1
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>f g : α → ℝ≥0∞<VAR>Hlt : ∀ i ∈ s, f i < g i<GOAL>∑ i ∈ s, f i < ∑ i ∈ s, g i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Preorder α<VAR>f : β → γ<VAR>g : α → Part β<VAR>hg : Antitone g<GOAL>Antitone fun x => map f (g x)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<GOAL>(∀ (I : Finset ι), ∃ r > 0, ∀ x ∈ s, (I.sup p) x < r) ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r<VAR>I : Finset ι<VAR>hI : ¬I.Nonempty<GOAL>∃ r > 0, ∀ x ∈ s, (I.sup p) x < r
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>s : Set E<VAR>hp : WithSeminorms p<VAR>hi : ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r<VAR>I : Finset ι<VAR>hI : ¬I.Nonempty<GOAL>∃ r > 0, ∀ x ∈ s, 0 < r
<VAR>r p : ℝ≥0<VAR>h : 1 ≤ r * p<GOAL>r⁻¹ ≤ p
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>IsIso f ↔ IsIso f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>((Epi f.val.base ∧ OpenEmbedding ⇑f.val.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)) ↔ IsIso f.val.base ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>Epi f.val.base ∧ OpenEmbedding ⇑f.val.base → IsIso f.val.base
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z : Scheme<VAR>f✝ : X✝ ⟶ Z<VAR>g : Y✝ ⟶ Z<VAR>H : IsOpenImmersion f✝<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>IsIso f.val.base → Epi f.val.base ∧ OpenEmbedding ⇑f.val.base
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<GOAL>M ↾ (M ↾ R).E = M ↾ R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : PseudoMetricSpace α<VAR>inst✝³ : ProperSpace α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a z : α<VAR>r : ℝ<VAR>hf : ContinuousOn f (closedBall a r)<VAR>hz : z ∈ closedBall a r<VAR>hf1 : ∀ z' ∈ sphere a r, f z < f z'<GOAL>∃ z ∈ ball a r, IsLocalMin f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : PseudoMetricSpace α<VAR>inst✝³ : ProperSpace α<VAR>x : α<VAR>r✝ : ℝ<VAR>s : Set α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : ConditionallyCompleteLinearOrder β<VAR>inst✝ : OrderTopology β<VAR>f : α → β<VAR>a z : α<VAR>r : ℝ<VAR>hf : ContinuousOn f (closedBall a r)<VAR>hz : z ∈ closedBall a r<VAR>hf1 : ∀ z' ∈ closedBall a r \ ball a r, f z < f z'<GOAL>∃ z ∈ ball a r, IsLocalMin f z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>s = univ ↔ ∀ (x : α), x ∈ s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<GOAL>Measure.map (fun a i => f i (a i)) (Measure.pi μ) = Measure.pi ν
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<VAR>this : ∀ (i : ι), SigmaFinite (μ i)<GOAL>Measure.map (fun a i => f i (a i)) (Measure.pi μ) = Measure.pi ν
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<VAR>this : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (β i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.map (fun a i => f i (a i)) (Measure.pi μ)) (univ.pi s) = ∏ i : ι, (ν i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<VAR>this : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (β i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>∏ i : ι, (μ i) (f i ⁻¹' s i) = ∏ i : ι, (ν i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<VAR>this : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (β i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>Measurable fun a i => f i (a i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝⁴ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝³ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝² : Fintype ι'<VAR>β : ι → Type u_4<VAR>inst✝¹ : (i : ι) → MeasurableSpace (β i)<VAR>ν : (i : ι) → Measure (β i)<VAR>f : (i : ι) → α i → β i<VAR>inst✝ : ∀ (i : ι), SigmaFinite (ν i)<VAR>hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)<VAR>this : ∀ (i : ι), SigmaFinite (μ i)<VAR>s : (i : ι) → Set (β i)<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<GOAL>MeasurableSet (univ.pi s)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>hu : ∀ (n : ι), Integrable (u n) μ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<GOAL>Integrable (stoppedValue u τ) μ
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>τ σ : Ω → ι<VAR>E : Type u_4<VAR>p : ℝ≥0∞<VAR>u : ι → Ω → E<VAR>inst✝¹ : PartialOrder ι<VAR>ℱ : Filtration ι m<VAR>inst✝ : NormedAddCommGroup E<VAR>hτ : IsStoppingTime ℱ τ<VAR>s : Finset ι<VAR>hbdd : ∀ (ω : Ω), τ ω ∈ s<VAR>hu : ∀ (n : ι), Memℒp (u n) 1 μ<GOAL>Memℒp (stoppedValue u τ) 1 μ
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>F : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace K F<VAR>f : E ≃ₗ[K] F<VAR>x : F<GOAL>x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ fundamentalDomain (b.map f)
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : NormedLinearOrderedField K<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace K E<VAR>b : Basis ι K E<VAR>F : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace K F<VAR>f : E ≃ₗ[K] F<VAR>x : F<GOAL>x ∈ ⇑f '' fundamentalDomain b ↔ x ∈ ⇑f.toEquiv '' fundamentalDomain b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<GOAL>0 < count a s ↔ a ∈ s
<VAR>m k : ℕ+<GOAL>↑(k.modDivAux (↑m % ↑k) (↑m / ↑k)).1 = if ↑m % ↑k = 0 then ↑k else ↑m % ↑k
<VAR>a : Ordinal.{u_1}<GOAL>nfp (fun x => a + x) 0 = a * ω
<VAR>a : Ordinal.{u_1}<GOAL>(sup fun n => (fun x => a + x)^[n] 0) = sup fun n => a * ↑n
<VAR>a : Ordinal.{u_1}<GOAL>(fun n => (fun x => a + x)^[n] 0) = fun n => a * ↑n
<VAR>a : Ordinal.{u_1}<VAR>n : ℕ<GOAL>(fun x => a + x)^[n] 0 = a * ↑n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>↑(Submodule.toAddSubgroup I).index = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<GOAL>↑(if h : Finite (R ⧸ Submodule.toAddSubgroup I) then Fintype.card (R ⧸ Submodule.toAddSubgroup I) else 0) = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hq : Finite (R ⧸ Submodule.toAddSubgroup I)<VAR>this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)<GOAL>↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{u₂, u₁} C<VAR>inst✝⁴ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝³ : FiberFunctor F<VAR>X Y Z : C<VAR>inst✝² : IsConnected X<VAR>inst✝¹ : IsGalois Y<VAR>inst✝ : IsGalois Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>autMap (f ≫ g) = autMap g ∘ autMap f
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{u₂, u₁} C<VAR>inst✝⁴ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝³ : FiberFunctor F<VAR>X Y Z : C<VAR>inst✝² : IsConnected X<VAR>inst✝¹ : IsGalois Y<VAR>inst✝ : IsGalois Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>σ : Aut X<GOAL>(f ≫ g) ≫ ((autMap g ∘ autMap f) σ).hom = σ.hom ≫ f ≫ g
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{u₂, u₁} C<VAR>inst✝⁴ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝³ : FiberFunctor F<VAR>X Y Z : C<VAR>inst✝² : IsConnected X<VAR>inst✝¹ : IsGalois Y<VAR>inst✝ : IsGalois Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>σ : Aut X<GOAL>(f ≫ (autMap f σ).hom) ≫ g = σ.hom ≫ f ≫ g
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>A : ι → Submodule R M<VAR>inst✝ : DecidableEq M<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(coeLinearMap A) x = DFinsupp.sum x fun i x => ↑x
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>A : ι → Submodule R M<VAR>inst✝ : DecidableEq M<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(DFinsupp.sumAddHom fun i => (A i).subtype.toAddMonoidHom) x = DFinsupp.sum x fun i x => ↑x
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>A : ι → Submodule R M<VAR>inst✝ : DecidableEq M<VAR>x : ⨁ (i : ι), ↥(A i)<GOAL>(DFinsupp.sum x fun x => ⇑(A x).subtype.toAddMonoidHom) = DFinsupp.sum x fun i x => ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>IsBigOWith c l (fun x => -f' x) g ↔ IsBigOWith c l f' g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<VAR>hσ : {x | σ x ≠ x} ⊆ ↑s<GOAL>∑ i ∈ s, f i • g i < ∑ i ∈ s, f (σ i) • g i ↔ ¬AntivaryOn (f ∘ ⇑σ) g ↑s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a r : ℝ<GOAL>0 < r ∧ x ∈ r • s ↔ r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{?u.21579, u_2} D<VAR>W : MorphismProperty C<VAR>X Y : C<VAR>z : W.LeftFraction X Y<GOAL>W (z.s ≫ 𝟙 z.Y')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f✝ f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>hc : ContinuousWithinAt f s x<GOAL>𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x = 𝓝[(extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)] ↑(extChartAt I x) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f✝ f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>f : M → M'<VAR>x : M<VAR>hc : ContinuousWithinAt f s x<GOAL>f ⁻¹' (extChartAt I' (f x)).source ∈ 𝓝[s] x
<VAR>a : ℤ<VAR>b : ℕ<VAR>h : a.gcd ↑b = 1<GOAL>J(a | b) ^ 2 = 1
<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.13, u_1} A<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>inst✝ : PreservesFiniteProducts F<VAR>hF : EqualizerCondition F<GOAL>IsSheaf (coherentTopology LightProfinite) F
<VAR>A : Type u_1<VAR>inst✝¹ : Category.{?u.13, u_1} A<VAR>F : LightProfiniteᵒᵖ ⥤ A<VAR>inst✝ : PreservesFiniteProducts F<VAR>hF : EqualizerCondition F<GOAL>Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : Integrable f μ<GOAL>Integrable g ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure α<VAR>ν : Measure β<VAR>f : α → γ<VAR>g : β → γ<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>inst✝ : BorelSpace γ<VAR>h : IdentDistrib f g μ ν<VAR>hf : Memℒp f 1 μ<GOAL>Memℒp g 1 ν
<VAR>H✝ : Type u<VAR>H'✝ : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>H : Type u_5<VAR>H' : Type u_6<VAR>α : Type u_7<VAR>f : H → α<GOAL>(range fun p => (f p.1, p.2)) = range f ×ˢ univ
<VAR>H✝ : Type u<VAR>H'✝ : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>H : Type u_5<VAR>H' : Type u_6<VAR>α : Type u_7<VAR>f : H → α<GOAL>(range fun p => (f p.1, p.2)) = range fun p => (f p.1, p.2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).sublists = do let x ← l₂.sublists map (fun x_1 => x_1 ++ x) l₁.sublists
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<GOAL>foldr (fun a acc => acc.bind fun x => [x, a :: x]) (foldr (fun a acc => acc.bind fun x => [x, a :: x]) [[]] l₂) l₁ = do let x ← foldr (fun a acc => acc.bind fun x => [x, a :: x]) [[]] l₂ map (fun x_1 => x_1 ++ x) (foldr (fun a acc => acc.bind fun x => [x, a :: x]) [[]] l₁)
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>p < p.succAbove i ↔ p ≤ i.castSucc
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>H : i.castSucc < p<GOAL>p < p.succAbove i ↔ p ≤ i.castSucc
<VAR>n m : ℕ<VAR>p✝ : Fin (n + 1)<VAR>i✝ j : Fin n<VAR>p : Fin (n + 1)<VAR>i : Fin n<VAR>H : p < i.succ<GOAL>p < p.succAbove i ↔ p ≤ i.castSucc
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<GOAL>p.comp (↑f).attachBound ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<GOAL>p.comp (↑f).attachBound ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<VAR>frequently_mem_polynomials : ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring<GOAL>p.comp (↑f).attachBound ∈ A.topologicalClosure
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<VAR>frequently_mem_polynomials : ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring<GOAL>∃ᶠ (x : C(X, ℝ)) in nhds (p.comp (↑f).attachBound), x ∈ ↑A.toSubsemiring
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<VAR>frequently_mem_polynomials : ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring<GOAL>∀ x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring, (compRightContinuousMap ℝ (↑f).attachBound) x ∈ ↑A.toSubsemiring
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>p : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)<VAR>mem_closure : p ∈ (polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).topologicalClosure<VAR>frequently_mem_polynomials : ∃ᶠ (x : C(↑(Set.Icc (-‖f‖) ‖f‖), ℝ)) in nhds p, x ∈ ↑(polynomialFunctions (Set.Icc (-‖f‖) ‖f‖)).toSubsemiring<VAR>g : ℝ[X]<GOAL>(compRightContinuousMap ℝ (↑f).attachBound) (↑(Polynomial.toContinuousMapOnAlgHom (Set.Icc (-‖f‖) ‖f‖)) g) ∈ ↑A.toSubsemiring