ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1<VAR>h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>∏ x ∈ f.support ∪ g.support, h x ((f + g) x) = ∏ x ∈ f.support ∪ g.support, h x (f x) * h x (g 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>x : M<VAR>h : x ∈ f.source<GOAL>x ∈ (f.extend I).source
<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>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<VAR>x : R<GOAL>(leftShiftLinearEquiv R K L n a n' hn).symm (x • γ) = x • γ.leftUnshift n hn
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NonUnitalNormedRing A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : SMulCommClass 𝕜 A A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : 𝓜(𝕜, A)<GOAL>‖a.toProd.1‖ = ‖a‖
<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 : ℤ<VAR>φ : F ⟶ G<VAR>p : ℤ<GOAL>(ofHom φ).v p p ⋯ = φ.f p
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u}<GOAL>lift.{u + 1, u} c < univ.{u, u + 1}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>U : Type u_2<VAR>inst✝¹ : CommRing U<VAR>inst✝ : Algebra R U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>h'' : IsAdjoinRoot U f<VAR>z : S<GOAL>((h.aequiv h').trans (h'.aequiv h'')) z = (h.aequiv h'') z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>s : Set β<VAR>h : LeftInvOn f g s<VAR>hx : f (g x) = x<VAR>hf : ContinuousWithinAt f (g '' s) (g x)<VAR>hg : ContinuousWithinAt g s x<GOAL>map g (𝓝[s] x) = 𝓝[g '' s] g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>s : Set β<VAR>h : LeftInvOn f g s<VAR>hx : f (g x) = x<VAR>hf : ContinuousWithinAt f (g '' s) (g x)<VAR>hg : ContinuousWithinAt g s x<GOAL>map g (𝓝[s] x) ≤ 𝓝[g '' s] g x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>g : β → α<VAR>x : β<VAR>s : Set β<VAR>h : LeftInvOn f g s<VAR>hx : f (g x) = x<VAR>hf : ContinuousWithinAt f (g '' s) (g x)<VAR>hg : ContinuousWithinAt g s x<GOAL>𝓝[g '' s] g x ≤ map g (𝓝[s] x)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>h_ifs✝ : ¬y = 0<VAR>h_ifs : ¬x = 0<GOAL>rexp (log (x * y) * z) = rexp (log x * z) * y ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>h_ifs : ¬x = 0 ∧ ¬y = 0<GOAL>0 ≤ x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<GOAL>0 ≤ x * y
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>m : ℕ<VAR>x : K<VAR>n : ℕ<VAR>y : K<VAR>z : ℕ<VAR>H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y<GOAL>mk K p (m, x) = mk K p (n, y)
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>m : ℕ<VAR>x : K<VAR>n : ℕ<VAR>y : K<VAR>z : ℕ<VAR>H : (⇑(frobenius K p))^[n + z] x = (⇑(frobenius K p))^[m + z] y<GOAL>mk K p (n + z + m, (⇑(frobenius K p))^[m + z] y) = mk K p (m + z + n, (⇑(frobenius K p))^[m + z] y)
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x y<VAR>H2 : x ∣ y * z<VAR>a b : R<VAR>H : a * x + b * y = 1<GOAL>x ∣ z
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H1 : IsCoprime x y<VAR>H2 : x ∣ y * z<VAR>a b : R<VAR>H : a * x + b * y = 1<GOAL>x ∣ a * z * x + b * (y * z)
<VAR>α β : Type u<VAR>c : Cardinal.{u_1}<GOAL>1 ≤ c ↔ c ≠ 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Set X)<VAR>hs : s.Finite<VAR>x✝ : ∀ t ∈ ∅, IsOpen t<GOAL>IsOpen (⋂₀ ∅)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Set X)<VAR>hs : s.Finite<VAR>x✝ : ∀ t ∈ ∅, IsOpen t<GOAL>IsOpen univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝¹ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Set X)<VAR>hs : s.Finite<VAR>a✝ : Set X<VAR>s✝ : Set (Set X)<VAR>x✝¹ : a✝ ∉ s✝<VAR>x✝ : s✝.Finite<VAR>ih : (∀ t ∈ s✝, IsOpen t) → IsOpen (⋂₀ s✝)<VAR>h : ∀ t ∈ insert a✝ s✝, IsOpen t<GOAL>IsOpen (⋂₀ insert a✝ s✝)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝¹ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (Set X)<VAR>hs : s.Finite<VAR>a✝ : Set X<VAR>s✝ : Set (Set X)<VAR>x✝¹ : a✝ ∉ s✝<VAR>x✝ : s✝.Finite<VAR>ih : (∀ t ∈ s✝, IsOpen t) → IsOpen (⋂₀ s✝)<VAR>h : IsOpen a✝ ∧ ∀ x ∈ s✝, IsOpen x<GOAL>IsOpen (a✝ ∩ ⋂₀ s✝)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : 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>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>S : Set X<GOAL>EquicontinuousOn F S ↔ ContinuousOn (⇑UniformFun.ofFun ∘ swap F) S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<GOAL>Continuous fun a => a ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<GOAL>∀ (x : ℝ≥0∞), ContinuousAt (fun a => a ^ n * a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<VAR>x : ℝ≥0∞<GOAL>ContinuousAt (fun a => a ^ n * a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<VAR>x : ℝ≥0∞<VAR>H : x = 0<GOAL>x ^ n ≠ 0 ∨ x ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<VAR>x : ℝ≥0∞<VAR>H : ¬x = 0<GOAL>x ^ n ≠ 0 ∨ x ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<VAR>x : ℝ≥0∞<VAR>H : x = 0<GOAL>x ≠ 0 ∨ x ^ n ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>n : ℕ<VAR>IH : Continuous fun a => a ^ n<VAR>x : ℝ≥0∞<VAR>H : ¬x = 0<GOAL>x ≠ 0 ∨ x ^ n ≠ ⊤
<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>Φ : α → β<GOAL>infDist x {y} = dist x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s : Finset β<VAR>h : Fintype.card α ≤ s.card<GOAL>∃ f, Set.range ⇑f ⊆ ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s : Finset β<VAR>h : Fintype.card α ≤ Fintype.card { x // x ∈ s }<GOAL>∃ f, Set.range ⇑f ⊆ ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Fintype α<VAR>s : Finset β<VAR>h : Fintype.card α ≤ Fintype.card { x // x ∈ s }<VAR>f : α ↪ { x // x ∈ s }<GOAL>∃ f, Set.range ⇑f ⊆ ↑s
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>m : M<VAR>s : ↥S<GOAL>0 • mk m s = 0
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => x - a) ⁻¹' Ici b = Ici (b + a)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_5, u_1} C<VAR>inst✝ : Category.{?u.41420, u_2} D<VAR>F G H : C ⥤ Cat<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>map (α ≫ β) = map α ⋙ map β
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_5, u_1} C<VAR>inst✝ : Category.{?u.41420, u_2} D<VAR>F G H : C ⥤ Cat<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_5, u_1} C<VAR>inst✝ : Category.{?u.41420, u_2} D<VAR>F G H : C ⥤ Cat<VAR>α : F ⟶ G<VAR>β : G ⟶ H<GOAL>autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯) _auto✝
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.4635) (N : Type ?u.4634) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Ico a b * Icc c d ⊆ Ico (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.4635) (N : Type ?u.4634) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : a ≤ y<VAR>hyb : y < b<VAR>z : α<VAR>hzc : c ≤ z<VAR>hzd : z ≤ d<GOAL>(fun x x_1 => x * x_1) y z ∈ Ico (a * c) (b * d)
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ map (fun h => g / h) μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ map (fun h => g * h⁻¹) μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ map (fun x => g * x) (map Inv.inv μ)
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>map (fun x => g * x) μ ≪ map (fun x => g * x) (map Inv.inv μ)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ<VAR>inst✝¹ : CommRing R<VAR>ζ✝ : Rˣ<VAR>h✝ : IsPrimitiveRoot ζ✝ k<VAR>inst✝ : IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>hn : ¬n = 0<GOAL>nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>inst✝¹ : HasLimits C<VAR>inst✝ : PreservesLimits T<VAR>A P : StructuredArrow S T<VAR>f : P ⟶ A<VAR>hf : Mono f<GOAL>(P.hom ≫ T.map (Subobject.underlyingIso f.right).inv) ≫ T.map (Subobject.mk f.right).arrow = A.hom
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>m n : ℤ<GOAL>↑(m - n) = ↑m - ↑n
<VAR>n : ℕ<VAR>σ : Perm (Fin n)<GOAL>map (⇑σ) (finRange n) ~ finRange n
<VAR>n : ℕ<VAR>σ : Perm (Fin n)<GOAL>∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>A : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} A<VAR>A' : Type u₂<VAR>inst✝⁴ : Category.{max v₁ u₁, u₂} A'<VAR>B : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} B<VAR>J : GrothendieckTopology C<VAR>U : C<VAR>R : Presieve U<VAR>P : Cᵒᵖ ⥤ A<VAR>P' : Cᵒᵖ ⥤ A'<VAR>s : A ⥤ B<VAR>inst✝² : HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A<VAR>inst✝¹ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s<VAR>inst✝ : s.ReflectsIsomorphisms<VAR>this : ReflectsLimitsOfSize.{v₁, max u₁ v₁, v₂, v₃, u₂, u₃} s := reflectsLimitsOfReflectsIsomorphisms<GOAL>IsSheaf J P ↔ IsSheaf J (P ⋙ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>w✝ : ι<VAR>hf : f w✝ = sup f<GOAL>succ (sup f) ≤ lsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v}<VAR>w✝ : ι<VAR>hf : f w✝ = sup f<GOAL>f w✝ < lsub f
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>𝒢 : Set Cᵒᵖ<GOAL>IsCoseparating 𝒢.unop ↔ IsSeparating 𝒢
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : P.Cotangent<GOAL>(CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Cotangent.map f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type u'<VAR>S' : Type v'<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type u''<VAR>S'' : Type v''<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>x : ↥P.ker<GOAL>(CotangentSpace.map f) (P.cotangentComplex (Cotangent.mk x)) = P'.cotangentComplex ((Cotangent.map f) (Cotangent.mk x))
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>((Functor.const J).obj ↑F.sections).map f ≫ (fun j u => ↑u j) j' = (fun j u => ↑u j) j ≫ F.map f
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ((Functor.const J).obj ↑F.sections).obj j<GOAL>(((Functor.const J).obj ↑F.sections).map f ≫ (fun j u => ↑u j) j') x = ((fun j u => ↑u j) j ≫ F.map f) x
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((PreservesCoequalizer.iso (tensorRight S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.mul ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫ (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv) ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(tensorRight S.X).map (coequalizer.π ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X R.X P.X).hom ≫ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft)) ≫ ((PreservesCoequalizer.iso (tensorRight S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.mul ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫ (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv) ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = (tensorRight S.X).map (coequalizer.π ({ X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actRight ▷ P.X) ((α_ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X R.X P.X).hom ≫ { X := R.X, actLeft := R.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := R.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X ◁ P.actLeft)) ≫ coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫ ((PreservesCoequalizer.iso (tensorRight S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft)).inv ≫ colimMap (parallelPairHom (R.mul ▷ P.X ▷ S.X) (((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X) (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ((α_ (R.X ⊗ R.X) P.X S.X).hom ≫ (α_ R.X R.X (P.X ⊗ S.X)).hom ≫ R.X ◁ R.X ◁ P.actRight ≫ (α_ R.X R.X P.X).inv) ((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ⋯ ⋯)) ≫ coequalizer.desc P.actLeft ⋯ = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫ coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft = coequalizer.π (R.mul ▷ P.X) ((α_ R.X R.X P.X).hom ≫ R.X ◁ P.actLeft) ▷ S.X ≫ coequalizer.desc P.actLeft ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft = P.actLeft ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight) ≫ P.actLeft = (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft
<VAR>cs cs' : List Char<VAR>i p : Nat<VAR>hp : i + utf8Len cs = p<GOAL>utf8GetAux? (cs ++ cs') { byteIdx := i } { byteIdx := p } = cs'.head?