ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s = μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<GOAL>μ' s ≤ μ'.haarScalarFactor μ • μ s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : ν (t \ s) ≤ μ' (t \ s)<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : ν (t \ s) ≤ μ' (t \ s)<VAR>B : μ' t = ν t<GOAL>μ' s ≤ ν s
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : μ' t - ν s ≤ μ' t - μ' s<VAR>B : μ' t = ν t<GOAL>μ' s ≤ μ' t
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : μ' t - ν s ≤ μ' t - μ' s<VAR>B : μ' t = ν t<GOAL>μ' t ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : ν t - ν s ≤ μ' (t \ s)<VAR>B : μ' t = ν t<GOAL>μ' s ≠ ⊤
<VAR>G : Type u_1<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : Group G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>inst✝⁴ : LocallyCompactSpace G<VAR>μ' μ : Measure G<VAR>inst✝³ : μ.IsHaarMeasure<VAR>inst✝² : IsFiniteMeasureOnCompacts μ'<VAR>inst✝¹ : μ'.IsMulLeftInvariant<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>s : Set G<VAR>hs : MeasurableSet s<VAR>h's : IsCompact (closure s)<VAR>ν : Measure G := μ'.haarScalarFactor μ • μ<VAR>f : G → ℝ<VAR>f_cont : Continuous f<VAR>hf : EqOn (⇑{ toFun := f, continuous_toFun := f_cont }) 1 (closure s)<VAR>f_comp : HasCompactSupport ⇑{ toFun := f, continuous_toFun := f_cont }<VAR>t : Set G := f ⁻¹' {1}<VAR>t_closed : IsClosed t<VAR>t_comp : IsCompact t<VAR>st : s ⊆ t<VAR>A : ν (t \ s) ≤ μ' (t \ s)<VAR>B : μ' t = ν t<GOAL>ν s ≠ ⊤
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝¹ : f.IsCountablyGenerated<VAR>inst✝ : f.NeBot<GOAL>∃ x, Tendsto x atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝¹ : f.IsCountablyGenerated<VAR>inst✝ : f.NeBot<VAR>B : ℕ → Set α<VAR>h : f.HasAntitoneBasis B<GOAL>∃ x, Tendsto x atTop f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : Filter α<VAR>inst✝¹ : f.IsCountablyGenerated<VAR>inst✝ : f.NeBot<VAR>B : ℕ → Set α<VAR>h : f.HasAntitoneBasis B<VAR>x : ℕ → α<VAR>hx : ∀ (n : ℕ), x n ∈ B n<GOAL>∃ x, Tendsto x atTop f
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Summable fun i => ‖f i‖ ^ p.toReal<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Summable fun i => ‖f i‖ ^ ENNReal.toReal 0<GOAL>Memℓp f 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Summable fun i => ‖f i‖ ^ ⊤.toReal<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Summable fun i => ‖f i‖ ^ p.toReal<VAR>hp : 0 < p.toReal<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CharZero α<VAR>m n : ℕ<GOAL>↑n ≤ 1 ↔ n ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>Irreducible (↑a * b) ↔ Irreducible b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : Monoid α<VAR>a : αˣ<VAR>b : α<GOAL>¬IsUnit b → ((∀ (a_2 b_1 : α), ↑a * b = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔ ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.42681, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>e f : ℤ<VAR>hf : -1 + e = f<VAR>γ : Cochain G K e<VAR>he : 0 + e = e<GOAL>(inl φ).comp ((snd φ).comp γ he) hf = 0
<VAR>α β : Type u<VAR>c : Cardinal.{?u.212142}<VAR>n : ℕ<GOAL>#α = ↑n ↔ ∃ h, Fintype.card α = n
<VAR>α β : Type u<VAR>c : Cardinal.{?u.212142}<VAR>n : ℕ<GOAL>(∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n
<VAR>l m r : List Char<VAR>it₁ it₂ : Iterator<VAR>h₁ : ValidFor l (m ++ r) it₁<VAR>h₂ : ValidFor (m.reverse ++ l) r it₂<GOAL>it₁.extract it₂ = { data := m }
<VAR>l m r : List Char<VAR>it₂ : Iterator<VAR>h₂ : ValidFor (m.reverse ++ l) r it₂<VAR>h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }<GOAL>{ s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract it₂ = { data := m }
<VAR>l m r : List Char<VAR>h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }<VAR>h₂ : ValidFor (m.reverse ++ l) r { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }<GOAL>{ s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }.extract { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } } = { data := m }
<VAR>l m r : List Char<VAR>h₁ : ValidFor l (m ++ r) { s := { data := l.reverseAux (m ++ r) }, i := { byteIdx := utf8Len l } }<VAR>h₂ : ValidFor (m.reverse ++ l) r { s := { data := (m.reverse ++ l).reverseAux r }, i := { byteIdx := utf8Len (m.reverse ++ l) } }<GOAL>{ data := l.reverse ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len m + utf8Len l } = { data := m }
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝⁹ : Category.{u_7, u_1} C<VAR>inst✝⁸ : Category.{u_6, u_2} D<VAR>inst✝⁷ : Category.{?u.20890, u_3} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁶ : AddMonoid A<VAR>inst✝⁵ : AddCommMonoid B<VAR>inst✝⁴ : HasShift C A<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : HasShift C B<VAR>inst✝ : HasShift D B<VAR>a b : A<VAR>e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a<VAR>e₂ : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b<VAR>X : C<GOAL>(isoAdd e₁ e₂).hom.app X = F.map ((shiftFunctorAdd C a b).hom.app X) ≫ e₂.hom.app ((shiftFunctor C a).obj X) ≫ (shiftFunctor D b).map (e₁.hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>star x < 1 ↔ x < 1
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c x✝¹ x✝ : ℍ[R,c₁,c₂]<GOAL>{ toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝¹ * x✝) = { toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun x✝¹ * { toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun x✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c x✝¹ x✝ : ℍ[R,c₁,c₂]<GOAL>{ toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun (x✝¹ + x✝) = { toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun x✝¹ + { toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun x✝
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<VAR>x✝ : R<GOAL>{ toFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, invFun := fun t => { re := t.re, imI := t.imJ, imJ := t.imI, imK := -t.imK }, left_inv := ⋯, right_inv := ⋯ }.toFun ((algebraMap R ℍ[R,c₁,c₂]) x✝) = (algebraMap R ℍ[R,c₂,c₁]) x✝
<VAR>M : Type u<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module ℤ M<VAR>inst✝ : Finite ℤ M<VAR>hM : IsTorsion ℤ M<GOAL>_root_.Finite M
<VAR>M : Type u<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module ℤ M<VAR>inst✝ : Finite ℤ M<VAR>hM : IsTorsion ℤ M<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>p : ι → ℤ<VAR>h : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<GOAL>_root_.Finite M
<VAR>M : Type u<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module ℤ M<VAR>inst✝ : Finite ℤ M<VAR>hM : IsTorsion ℤ M<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>p : ι → ℤ<VAR>h : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<VAR>this : ∀ (i : ι), NeZero (p i ^ e i).natAbs<GOAL>_root_.Finite M
<VAR>M : Type u<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module ℤ M<VAR>inst✝ : Finite ℤ M<VAR>hM : IsTorsion ℤ M<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>p : ι → ℤ<VAR>h : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<VAR>this✝ : ∀ (i : ι), NeZero (p i ^ e i).natAbs<VAR>this : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})<GOAL>_root_.Finite M
<VAR>M : Type u<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module ℤ M<VAR>inst✝ : Finite ℤ M<VAR>hM : IsTorsion ℤ M<VAR>ι : Type<VAR>w✝ : Fintype ι<VAR>p : ι → ℤ<VAR>h : ∀ (i : ι), Irreducible (p i)<VAR>e : ι → ℕ<VAR>l : M ≃ₗ[ℤ] ⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i}<VAR>this✝¹ : ∀ (i : ι), NeZero (p i ^ e i).natAbs<VAR>this✝ : ∀ (i : ι), _root_.Finite (ℤ ⧸ Submodule.span ℤ {p i ^ e i})<VAR>this : _root_.Finite (⨁ (i : ι), ℤ ⧸ Submodule.span ℤ {p i ^ e i})<GOAL>_root_.Finite M
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : AddCommMonoid μ<VAR>inst✝⁴ : HasAntidiagonal μ<VAR>inst✝³ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝² : AddCommMonoid μ'<VAR>inst✝¹ : HasAntidiagonal μ'<VAR>inst✝ : DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ'<GOAL>f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) → f ∈ s.finsuppAntidiag (e n)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : AddCommMonoid μ<VAR>inst✝⁴ : HasAntidiagonal μ<VAR>inst✝³ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f✝ : ι →₀ μ<VAR>inst✝² : AddCommMonoid μ'<VAR>inst✝¹ : HasAntidiagonal μ'<VAR>inst✝ : DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ'<GOAL>(∃ a, ((a.sum fun x x => x) = n ∧ a.support ⊆ s) ∧ (mapRange.addEquiv e).toEmbedding a = f) → (f.sum fun x x => x) = e n ∧ f.support ⊆ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : AddCommMonoid μ<VAR>inst✝⁴ : HasAntidiagonal μ<VAR>inst✝³ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f : ι →₀ μ<VAR>inst✝² : AddCommMonoid μ'<VAR>inst✝¹ : HasAntidiagonal μ'<VAR>inst✝ : DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<VAR>g : ι →₀ μ<VAR>hsum : (g.sum fun x x => x) = n<VAR>hsupp : g.support ⊆ s<GOAL>(((mapRange.addEquiv e).toEmbedding g).sum fun x x => x) = e n ∧ ((mapRange.addEquiv e).toEmbedding g).support ⊆ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : AddCommMonoid μ<VAR>inst✝⁴ : HasAntidiagonal μ<VAR>inst✝³ : DecidableEq μ<VAR>s✝ : Finset ι<VAR>n✝ : μ<VAR>f : ι →₀ μ<VAR>inst✝² : AddCommMonoid μ'<VAR>inst✝¹ : HasAntidiagonal μ'<VAR>inst✝ : DecidableEq μ'<VAR>e : μ ≃+ μ'<VAR>s : Finset ι<VAR>n : μ<VAR>g : ι →₀ μ<VAR>hsum : (g.sum fun x x => x) = n<VAR>hsupp : g.support ⊆ s<GOAL>((mapRange ⇑e ⋯ g).sum fun x x => x) = e n ∧ (mapRange ⇑e ⋯ g).support ⊆ s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ x y : List α<GOAL>x ++ y = y ↔ x = []
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>Surjective ⇑f.rangeRestrict
<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>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).degree = p.degree
<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>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>(k • p).degree ≤ p.degree
<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>S : Type u_1<VAR>inst✝¹ : Monoid S<VAR>inst✝ : DistribMulAction S R<VAR>k : S<VAR>p : R[X]<VAR>h : IsSMulRegular R k<GOAL>p.degree ≤ (k • p).degree
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<GOAL>(↑p ^ n * c).valuation = ↑n + c.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<VAR>this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖<GOAL>(↑p ^ n * c).valuation = ↑n + c.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<VAR>this : ‖↑p ^ n * c‖ = ‖↑p ^ n‖ * ‖c‖<VAR>aux : ↑p ^ n * c ≠ 0<GOAL>(↑p ^ n * c).valuation = ↑n + c.valuation
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<VAR>this : ↑p ^ (-(↑p ^ n * c).valuation) = ↑p ^ (-(↑n + c.valuation))<VAR>aux : ↑p ^ n * c ≠ 0<GOAL>0 < ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<VAR>this : ↑p ^ (-(↑p ^ n * c).valuation) = ↑p ^ (-(↑n + c.valuation))<VAR>aux : ↑p ^ n * c ≠ 0<GOAL>↑p ≠ 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>c : ℤ_[p]<VAR>hc : c ≠ 0<VAR>this : ↑p ^ (-(↑p ^ n * c).valuation) = ↑p ^ (-↑n) * ↑p ^ (-c.valuation)<VAR>aux : ↑p ^ n * c ≠ 0<GOAL>↑p ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t s : Set α<VAR>h : s.Infinite<VAR>this : Infinite ↑s<GOAL>s.encard = ⊤
<VAR>θ : Angle<GOAL>θ.cos < 0 ↔ π / 2 < |θ.toReal|
<VAR>α : Type u_1<VAR>inst✝ : SeminormedCommGroup α<VAR>n : ℤ<VAR>a : α<GOAL>‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℤ<GOAL>(W.baseChange B).φ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).φ n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>s : Set α<VAR>B : Set (Set α)<VAR>empty_mem : ∅ ∈ B<VAR>subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B<VAR>union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B<VAR>sUnion_univ : ∀ (x : α), {x} ∈ B<GOAL>IsBounded s ↔ s ∈ B
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>P.f_modif (1 / x) = (P.ε * ↑(x ^ P.k)) • P.g_modif x