ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>m : ℕ<GOAL>C (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) * W.ψ₂ * W.ψ₂ = (C (W.preΨ' (m + 2)) * if Even m then W.ψ₂ else 1) ^ 2 * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 5)) * if Even m then 1 else W.ψ₂) - (C (W.preΨ' (m + 1)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 3)) * if Even m then 1 else W.ψ₂) * (C (W.preΨ' (m + 4)) * if Even m then W.ψ₂ else 1) ^ 2
<VAR>E : Type u_1<VAR>L : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : AddCommGroup L<VAR>inst✝⁴ : Countable L<VAR>inst✝³ : AddAction L E<VAR>inst✝² : MeasurableSpace L<VAR>inst✝¹ : MeasurableVAdd L E<VAR>inst✝ : VAddInvariantMeasure L E μ<VAR>fund : IsAddFundamentalDomain L F μ<VAR>hS : NullMeasurableSet s μ<VAR>h : μ F < μ s<GOAL>∃ x y, x ≠ y ∧ ¬Disjoint (x +ᵥ s) (y +ᵥ s)
<VAR>E : Type u_1<VAR>L : Type u_2<VAR>inst✝⁶ : MeasurableSpace E<VAR>μ : Measure E<VAR>F s : Set E<VAR>inst✝⁵ : AddCommGroup L<VAR>inst✝⁴ : Countable L<VAR>inst✝³ : AddAction L E<VAR>inst✝² : MeasurableSpace L<VAR>inst✝¹ : MeasurableVAdd L E<VAR>inst✝ : VAddInvariantMeasure L E μ<VAR>fund : IsAddFundamentalDomain L F μ<VAR>hS : NullMeasurableSet s μ<VAR>h : ∀ (x y : L), x ≠ y → Disjoint (x +ᵥ s) (y +ᵥ s)<GOAL>μ s ≤ μ F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a✝ : α<GOAL>(toFinsupp (s ∩ t)) a✝ = (toFinsupp s ⊓ toFinsupp t) a✝
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : Cocone (coyoneda.obj X)<VAR>Y : C<GOAL>(colimitCocone X).ι.app Y ≫ (fun s x => s.ι.app (unop X) (𝟙 (unop X))) s = s.ι.app Y
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : Cocone (coyoneda.obj X)<VAR>Y : C<VAR>f : (coyoneda.obj X).obj Y<GOAL>((colimitCocone X).ι.app Y ≫ (fun s x => s.ι.app (unop X) (𝟙 (unop X))) s) f = s.ι.app Y f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : Cocone (coyoneda.obj X)<VAR>Y : C<VAR>f : (coyoneda.obj X).obj Y<VAR>e_1✝ : s.pt = ((Functor.const C).obj s.pt).obj (unop X)<GOAL>s.ι.app Y f = ((coyoneda.obj X).map f ≫ s.ι.app Y) (𝟙 (unop X))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : Cocone (coyoneda.obj X)<VAR>m : (colimitCocone X).pt ⟶ s.pt<VAR>w : ∀ (j : C), (colimitCocone X).ι.app j ≫ m = s.ι.app j<GOAL>m = (fun s x => s.ι.app (unop X) (𝟙 (unop X))) s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : Cᵒᵖ<VAR>s : Cocone (coyoneda.obj X)<VAR>m : (colimitCocone X).pt ⟶ s.pt<VAR>w : ∀ (j : C), (colimitCocone X).ι.app j ≫ m = s.ι.app j<GOAL>∀ (x : (colimitCocone X).pt), m x = (fun s x => s.ι.app (unop X) (𝟙 (unop X))) s x
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (rTensor Q ((range g).subtype ∘ₗ g.rangeRestrict)) = range (rTensor Q (range g).subtype)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (rTensor Q (range g).subtype ∘ₗ rTensor Q g.rangeRestrict) = range (rTensor Q (range g).subtype)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>range (rTensor Q g.rangeRestrict) = ⊤
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : AddCommMonoid Q<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>inst✝¹ : Module R P<VAR>inst✝ : Module R Q<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>this : g = (range g).subtype ∘ₗ g.rangeRestrict<GOAL>Function.Surjective ⇑(rTensor Q g.rangeRestrict)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝¹ : One M<VAR>inst✝ : One N<VAR>s✝ t : Set α<VAR>f g : α → M<VAR>a : α<VAR>s : Set α<GOAL>Disjoint (mulSupport fun x => 1) s
<VAR>o : Ordinal.{u_1}<GOAL>(sup fun n => o * ↑n) = o * ω
<GOAL>(sup fun n => 0 * ↑n) = 0 * ω
<VAR>o : Ordinal.{u_1}<VAR>ho : 0 < o<GOAL>(sup fun n => o * ↑n) = o * ω
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ F<VAR>i✝ : F<VAR>a✝ : i✝ ∈ f.range<GOAL>‖T (↑f ⁻¹' {i✝})‖ ≤ C * (μ (↑f ⁻¹' {i✝})).toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ F<GOAL>∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖ ≤ C * ∑ x ∈ f.range, (μ (↑f ⁻¹' {x})).toReal * ‖x‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → F →L[ℝ] F'<VAR>C : ℝ<VAR>hT_norm : ∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * (μ s).toReal<VAR>f : α →ₛ F<GOAL>∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖ ≤ ∑ x ∈ f.range, C * (μ (↑f ⁻¹' {x})).toReal * ‖x‖
<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>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s<GOAL>UniformEquicontinuousOn F S ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<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>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ x ∈ s ia, ((⇑UniformFun.ofFun ∘ swap F) x.1, (⇑UniformFun.ofFun ∘ swap F) x.2) ∈ UniformFun.gen ι α ib) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<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>p : κ → Prop<VAR>s : κ → Set (β × β)<VAR>F : ι → β → α<VAR>S : Set β<VAR>hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s<GOAL>(∀ ib ∈ 𝓤 α, ∃ ia, p ia ∧ ∀ (a b : β), (a, b) ∈ s ia → ((⇑UniformFun.ofFun ∘ swap F) a, (⇑UniformFun.ofFun ∘ swap F) b) ∈ UniformFun.gen ι α ib) ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x ^ y = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>(if ↑x = 0 then if ↑y = 0 then 1 else 0 else Complex.exp (Complex.log ↑x * ↑y)).re = if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>↑η ^ 2 = -↑η - 1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>↑η ^ 2 + ↑η + 1 = 0
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>↑(↑η ^ 2 + ↑η + 1) = ↑0
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : F<VAR>hy : y ≠ 0<GOAL>Set.InjOn Norm.norm {x | SameRay ℝ x y}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 0 → E<VAR>v' : Fin 0 → F<VAR>c : Composition 0 := Composition.ones 0<GOAL>(∑ c : Composition 0, q.compAlongComposition p c) v = (q 0) v'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 0 → E<VAR>v' : Fin 0 → F<VAR>c : Composition 0 := Composition.ones 0<VAR>this : {c} = Finset.univ<GOAL>(∑ c : Composition 0, q.compAlongComposition p c) v = (q 0) v'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>q : FormalMultilinearSeries 𝕜 F G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>v : Fin 0 → E<VAR>v' : Fin 0 → F<VAR>c : Composition 0 := Composition.ones 0<VAR>this : {c} = Finset.univ<GOAL>(q c.length) (p.applyComposition c v) = (q 0) v'
<VAR>a x✝ z x : ℂ<GOAL>↑(abs x) * cexp (↑x.arg * I) = x
<VAR>a x z : ℂ<GOAL>↑(abs 0) * cexp (↑(arg 0) * I) = 0
<VAR>a x✝ z x : ℂ<VAR>hx : x ≠ 0<GOAL>↑(abs x) * cexp (↑x.arg * I) = x
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>K⟮α⟯ = ⊤
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>⊤.toSubalgebra = Algebra.adjoin K {α}
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Injective ⇑f'<VAR>n : ℕ<GOAL>Injective ⇑(f' ^ (n + 1))
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Injective ⇑f'<VAR>n : ℕ<GOAL>Injective ⇑((f' ^ n) ∘ₗ f')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : s.SupIndep fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (g i').SupIndep f<GOAL>(s.sup g).SupIndep f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f<GOAL>(↑(s.sup g)).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>s✝ : Finset ι<VAR>f✝ : ι → α<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι'<VAR>g : ι' → Finset ι<VAR>f : ι → α<VAR>hs : (↑s).PairwiseDisjoint fun i => (g i).sup f<VAR>hg : ∀ i' ∈ s, (↑(g i')).PairwiseDisjoint f<GOAL>(⋃ x ∈ ↑s, ↑(g x)).PairwiseDisjoint f
<VAR>C : Type u_2<VAR>D : Type ?u.34421<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Category.{?u.34429, ?u.34421} D<VAR>X Y : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>(Sieve.pullback f T).arrows g ↔ ⊤.arrows g
<VAR>C : Type u_2<VAR>D : Type ?u.34421<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Category.{?u.34429, ?u.34421} D<VAR>X Y : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>T.arrows (g ≫ f)
<VAR>C : Type u_2<VAR>D : Type ?u.34421<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Category.{?u.34429, ?u.34421} D<VAR>X Y : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>S.arrows (g ≫ f)
<VAR>C : Type u_2<VAR>D : Type ?u.34421<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>inst✝ : Category.{?u.34429, ?u.34421} D<VAR>X Y : C<VAR>S T : Sieve X<VAR>h : S ≤ T<VAR>f : Y ⟶ X<VAR>hf : S.arrows f<VAR>Z : C<VAR>g : Z ⟶ Y<GOAL>S.arrows f
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<GOAL>PredOrder.limitRecOn (pred a) H_pred H_lim = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<VAR>h : ¬IsPredLimit (pred a)<GOAL>PredOrder.limitRecOn (pred a) H_pred H_lim = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<VAR>h : ¬IsPredLimit (pred a)<GOAL>(let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = pred a) ⋯; ⋯ ▸ H_pred ↑x ⋯ ((fun y x => ⋯.fix (fun a IH => if h : IsPredLimit a then H_lim a h IH else let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = a) ⋯; ⋯ ▸ H_pred ↑x ⋯ (IH ↑x ⋯)) y) ↑x ⋯)) = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<VAR>h : ¬IsPredLimit (pred a)<VAR>this : ∀ {b c : α} {hb : ¬IsMin b} {hc : ¬IsMin c} {x : (a : α) → C a} (h : b = c), ⋯ ▸ H_pred b hb (x b) = H_pred c hc (x c)<GOAL>(let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = pred a) ⋯; ⋯ ▸ H_pred ↑x ⋯ ((fun y x => ⋯.fix (fun a IH => if h : IsPredLimit a then H_lim a h IH else let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = a) ⋯; ⋯ ▸ H_pred ↑x ⋯ (IH ↑x ⋯)) y) ↑x ⋯)) = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>α : Type u_1<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : PredOrder α<VAR>a b : α<VAR>C : α → Sort u_2<VAR>inst✝ : WellFoundedGT α<VAR>H_pred : (a : α) → ¬IsMin a → C a → C (pred a)<VAR>H_lim : (a : α) → IsPredLimit a → ((b : α) → b > a → C b) → C a<VAR>ha : ¬IsMin a<VAR>h : ¬IsPredLimit (pred a)<VAR>this : ∀ {b c : α} {hb : ¬IsMin b} {hc : ¬IsMin c} {x : (a : α) → C a} (h : b = c), ⋯ ▸ H_pred b hb (x b) = H_pred c hc (x c)<VAR>x : { x // ¬IsMin x ∧ pred x = pred a } := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = pred a) ⋯<GOAL>(let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = pred a) ⋯; ⋯ ▸ H_pred ↑x ⋯ ((fun y x => ⋯.fix (fun a IH => if h : IsPredLimit a then H_lim a h IH else let x := Classical.indefiniteDescription (fun x => ¬IsMin x ∧ pred x = a) ⋯; ⋯ ▸ H_pred ↑x ⋯ (IH ↑x ⋯)) y) ↑x ⋯)) = H_pred a ha (PredOrder.limitRecOn a H_pred H_lim)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Precoherent C<VAR>W : C<GOAL>Presieve.IsSheaf (coherentTopology C) (yoneda.obj W)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Precoherent C<VAR>W : C<GOAL>∀ (B : C) (α : Type) [inst : Finite α] (X : α → C) (π : (a : α) → X a ⟶ B), EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<GOAL>Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generateFamily Y π).arrows.cocone<GOAL>Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone<GOAL>Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows Y π)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone<VAR>x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)<VAR>hx : x.Compatible<VAR>x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone<VAR>x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)<VAR>hx : x.Compatible<VAR>x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone<VAR>x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)<VAR>hx : x.Compatible<VAR>x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<VAR>S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)<GOAL>∃! t, x.IsAmalgamation t
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Precoherent C<VAR>W X : C<VAR>α : Type<VAR>inst✝ : Finite α<VAR>Y : α → C<VAR>π : (a : α) → Y a ⟶ X<VAR>H : EffectiveEpiFamily Y π<VAR>h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone<VAR>x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)<VAR>hx : x.Compatible<VAR>x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend<VAR>hx_ext : x.sieveExtend.Compatible<VAR>S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)<VAR>t : (yoneda.obj W).obj (Opposite.op X)<VAR>t_amalg : x_ext.IsAmalgamation t<VAR>t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t => x_ext.IsAmalgamation t) y → y = t<GOAL>∃! t, x.IsAmalgamation t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<VAR>h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1<VAR>h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)<GOAL>raise' (lower' (m :: l) n) n = m :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Denumerable α<VAR>inst✝ : Denumerable β<VAR>m : ℕ<VAR>l : List ℕ<VAR>n : ℕ<VAR>h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1<VAR>h₂ : Sorted (fun x x_1 => x < x_1) (m :: l)<VAR>this : n ≤ m<GOAL>raise' (lower' (m :: l) n) n = m :: l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α →₀ M<VAR>x✝ : α<GOAL>(filter p f) x✝ = {x | p x}.indicator (⇑f) x✝