ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(Seq.map ret s).join = s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>∀ (s : Seq α), BisimO (fun s1 s2 => ∃ s, s1 = (Seq.map ret s).join ∧ s2 = s) (Seq.map ret s).join.destruct s.destruct
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<GOAL>↑{a} ⊆ s ↔ a ∈ s
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<GOAL>∑ w : InfinitePlace K, w.mult = FiniteDimensional.finrank ℚ K
<VAR>k : Type u_1<VAR>inst✝³ : Field k<VAR>K : Type u_2<VAR>inst✝² : Field K<VAR>F : Type u_3<VAR>inst✝¹ : Field F<VAR>inst✝ : NumberField K<GOAL>∑ w : InfinitePlace K, w.mult = ∑ j : InfinitePlace K, ∑ i ∈ Finset.filter (fun i => mk i = j) Finset.univ, 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<GOAL>cofinite = ⊥ ↔ Finite α
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>coeff m (p * X s) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m✝ : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝ : DecidableEq σ<VAR>m : σ →₀ ℕ<VAR>s : σ<VAR>p : MvPolynomial σ R<GOAL>(if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) = if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<GOAL>(∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔ (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f = LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<GOAL>(∀ (x : M), f x * f x = (algebraMap R A) (Q x)) ↔ ∀ (x x_1 : M), (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 = ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<VAR>h : ∀ (x x_1 : M), (((LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f) x) x_1 = ((LinearMap.compr₂ (QuadraticMap.polarBilin Q) (Algebra.linearMap R A)) x) x_1<VAR>x : M<GOAL>f x * f x = (algebraMap R A) (Q x)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<VAR>x : M<VAR>h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)<GOAL>f x * f x = (algebraMap R A) (Q x)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A✝ : Type u_3<VAR>inst✝³ : Semiring A✝<VAR>inst✝² : Algebra R A✝<VAR>A : Type u_4<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>h2 : IsUnit 2<VAR>f : M →ₗ[R] A<VAR>x : M<VAR>h : ∀ (x y : M), f x * f y + f y * f x = (algebraMap R A) (QuadraticMap.polar (⇑Q) x y)<GOAL>2 * (f x * f x) = 2 * (algebraMap R A) (Q x)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : Fintype m<VAR>inst✝ : LinearOrderedField R<VAR>A : Matrix m n R<GOAL>(A * Aᵀ).rank = A.rank
<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>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>derivWithin (fun y => f y - c) s x = derivWithin f s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : ContinuousWithinAt (dslope f a) s b<GOAL>ContinuousWithinAt f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : ContinuousWithinAt (dslope f a) s b<VAR>this : ContinuousWithinAt (fun x => (x - a) • dslope f a x + f a) s b<GOAL>ContinuousWithinAt f s b
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g h : G<VAR>a : α<GOAL>g • a ∈ orbit G (h • a)
<VAR>f✝ g✝ f g : CircleDeg1Lift<VAR>h : f ≤ g<VAR>n : ℕ<GOAL>(f ^ n) 0 ≤ (g ^ n) 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - a) = p
<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<GOAL>isomorphisms Scheme f✝ ↔ (@IsOpenImmersion ⊓ @Surjective) f✝
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<GOAL>Nonempty (Path (IsFreeGroupoid.symgen a) (IsFreeGroupoid.symgen b))
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<GOAL>FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (IsFreeGroupoid.symgen a)))⁻¹ = 1
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<VAR>X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))<VAR>f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)<VAR>F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f<VAR>a✝ b✝ : Generators G<VAR>e✝ : a✝ ⟶ b✝<GOAL>F.map (of e✝) = ((Functor.const G).obj ()).map (of e✝)
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<VAR>X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))<VAR>f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)<VAR>F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f<VAR>a✝ b✝ : Generators G<VAR>e✝ : a✝ ⟶ b✝<GOAL>f b✝ = f (let_fun this := a✝; this)
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<VAR>X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))<VAR>f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)<VAR>F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f<VAR>a✝ b✝ : Generators G<VAR>e✝ : a✝ ⟶ b✝<GOAL>WeaklyConnectedComponent.mk b✝ = WeaklyConnectedComponent.mk (let_fun this := a✝; this)
<VAR>G : Type u<VAR>inst✝¹ : Groupoid G<VAR>inst✝ : IsFreeGroupoid G<VAR>a b : G<VAR>p : a ⟶ b<VAR>X : Type u := FreeGroup (WeaklyConnectedComponent (Generators G))<VAR>f : G → X := fun g => FreeGroup.of (WeaklyConnectedComponent.mk g)<VAR>F : G ⥤ CategoryTheory.SingleObj X := differenceFunctor f<VAR>a✝ b✝ : Generators G<VAR>e✝ : a✝ ⟶ b✝<GOAL>Nonempty (Path b✝ (let_fun this := a✝; this))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommSemiring P<VAR>A : Type u_4<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra A R<VAR>m : A<GOAL>mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra R S<VAR>P : Type u_3<VAR>inst✝² : CommSemiring P<VAR>A : Type u_4<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra A R<VAR>m : A<GOAL>(algebraMap R (Localization M)) ((algebraMap A R) m) = (algebraMap A (Localization M)) m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(cons a s h).erase a = s
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<VAR>hnm : n ≤ m<GOAL>Monotone fun n => lowerCrossingTime a b f N n ω
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{?u.62699, u_1} C<VAR>inst✝³ : Preadditive C<VAR>I₁ : Type u_2<VAR>I₂ : Type u_3<VAR>I₁₂ : Type u_4<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>K L M : HomologicalComplex₂ C c₁ c₂<VAR>φ : K ⟶ L<VAR>e : K ≅ L<VAR>ψ : L ⟶ M<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : DecidableEq I₁₂<VAR>inst✝¹ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝ : K.HasTotal c₁₂<VAR>i₁₂ i₁₂' : I₁₂<VAR>h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'<GOAL>K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂' = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>(algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 A
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>(algebraMap ℝ 𝕜) (hA.eigenvalues i) ∈ spectrum 𝕜 (toEuclideanLin A)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>IsIso (ModuleCat.ofHom (ofTensorProduct I M))
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Epi (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 0 ⋯)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 1 ⋯)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>IsIso (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 3 ⋯)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Mono (ComposableArrows.app' (AdicCompletion.firstRowToSecondRow I M f) 4 ⋯)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a⁻¹ ≤ b ↔ b⁻¹ ≤ a
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>r : F.M → Sort u_2<VAR>f : (x : ↑F F.M) → r (M.mk x)<VAR>fst✝ : F.A<VAR>snd✝ : F.B fst✝ → F.M<GOAL>f ⟨match 0, CofixA.intro fst✝ fun i => (snd✝ i).approx 0 with | x, CofixA.intro i a => i, fun i => children { approx := Approx.sMk ⟨fst✝, snd✝⟩, consistent := ⋯ } i⟩ = f ⟨fst✝, snd✝⟩
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>r : F.M → Sort u_2<VAR>f : (x : ↑F F.M) → r (M.mk x)<VAR>fst✝ : F.A<VAR>snd✝ : F.B fst✝ → F.M<GOAL>f = f
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G : A ⥤ D<VAR>H : B ⥤ E<VAR>K : C ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : D ⥤ E<VAR>R₂ : E ⥤ D<VAR>L₃ : B ⥤ C<VAR>R₃ : C ⥤ B<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : H ⋙ L₄ ⟶ L₃ ⋙ K<VAR>c : C<GOAL>({ toFun := fun α => whiskerLeft ((R₃ ⋙ R₁) ⋙ G) { homEquiv := fun X Z => (adj₄.homEquiv (L₂.obj X) Z).trans (adj₂.homEquiv X (R₄.obj Z)), unit := adj₂.unit ≫ whiskerLeft L₂ (whiskerRight adj₄.unit R₂) ≫ (L₂.associator (L₄ ⋙ R₄) R₂).inv, counit := (R₄.associator R₂ (L₂ ⋙ L₄)).hom ≫ whiskerLeft R₄ (whiskerRight adj₂.counit L₄) ≫ adj₄.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.unit ≫ whiskerRight (whiskerLeft (R₃ ⋙ R₁) α) (R₄ ⋙ R₂) ≫ whiskerRight { homEquiv := fun X Z => (adj₃.homEquiv (L₁.obj X) Z).trans (adj₁.homEquiv X (R₃.obj Z)), unit := adj₁.unit ≫ whiskerLeft L₁ (whiskerRight adj₃.unit R₁) ≫ (L₁.associator (L₃ ⋙ R₃) R₁).inv, counit := (R₃.associator R₁ (L₁ ⋙ L₃)).hom ≫ whiskerLeft R₃ (whiskerRight adj₁.counit L₃) ≫ adj₃.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.counit (K ⋙ R₄ ⋙ R₂), invFun := fun β => whiskerRight { homEquiv := fun X Z => (adj₃.homEquiv (L₁.obj X) Z).trans (adj₁.homEquiv X (R₃.obj Z)), unit := adj₁.unit ≫ whiskerLeft L₁ (whiskerRight adj₃.unit R₁) ≫ (L₁.associator (L₃ ⋙ R₃) R₁).inv, counit := (R₃.associator R₁ (L₁ ⋙ L₃)).hom ≫ whiskerLeft R₃ (whiskerRight adj₁.counit L₃) ≫ adj₃.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.unit (G ⋙ L₂ ⋙ L₄) ≫ whiskerRight (whiskerLeft (L₁ ⋙ L₃) β) (L₂ ⋙ L₄) ≫ whiskerLeft ((L₁ ⋙ L₃) ⋙ K) { homEquiv := fun X Z => (adj₄.homEquiv (L₂.obj X) Z).trans (adj₂.homEquiv X (R₄.obj Z)), unit := adj₂.unit ≫ whiskerLeft L₂ (whiskerRight adj₄.unit R₂) ≫ (L₂.associator (L₄ ⋙ R₄) R₂).inv, counit := (R₄.associator R₂ (L₂ ⋙ L₄)).hom ≫ whiskerLeft R₄ (whiskerRight adj₂.counit L₄) ≫ adj₄.counit, homEquiv_unit := ⋯, homEquiv_counit := ⋯ }.counit, left_inv := ⋯, right_inv := ⋯ } (whiskerRight α L₄ ≫ whiskerLeft L₁ β)).app c = (whiskerLeft R₃ ({ toFun := fun α => whiskerLeft (R₁ ⋙ G) adj₂.unit ≫ whiskerRight (whiskerLeft R₁ α) R₂ ≫ whiskerRight adj₁.counit (H ⋙ R₂), invFun := fun β => whiskerRight adj₁.unit (G ⋙ L₂) ≫ whiskerRight (whiskerLeft L₁ β) L₂ ≫ whiskerLeft (L₁ ⋙ H) adj₂.counit, left_inv := ⋯, right_inv := ⋯ } α) ≫ whiskerRight ({ toFun := fun α => whiskerLeft (R₃ ⋙ H) adj₄.unit ≫ whiskerRight (whiskerLeft R₃ α) R₄ ≫ whiskerRight adj₃.counit (K ⋙ R₄), invFun := fun β => whiskerRight adj₃.unit (H ⋙ L₄) ≫ whiskerRight (whiskerLeft L₃ β) L₄ ≫ whiskerLeft (L₃ ⋙ K) adj₄.counit, left_inv := ⋯, right_inv := ⋯ } β) R₂).app c
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G : A ⥤ D<VAR>H : B ⥤ E<VAR>K : C ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : D ⥤ E<VAR>R₂ : E ⥤ D<VAR>L₃ : B ⥤ C<VAR>R₃ : C ⥤ B<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : H ⋙ L₄ ⟶ L₃ ⋙ K<VAR>c : C<GOAL>adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))) = adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (α.app (R₁.obj (R₃.obj c))) ≫ R₂.map (H.map (adj₁.counit.app (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (H.obj (R₃.obj c))) ≫ R₂.map (R₄.map (β.app (R₃.obj c))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G : A ⥤ D<VAR>H : B ⥤ E<VAR>K : C ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : D ⥤ E<VAR>R₂ : E ⥤ D<VAR>L₃ : B ⥤ C<VAR>R₃ : C ⥤ B<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : H ⋙ L₄ ⟶ L₃ ⋙ K<VAR>c : C<GOAL>adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))) = adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ (R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c)))) ≫ R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c)) ≫ H.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (R₃.obj c)))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G : A ⥤ D<VAR>H : B ⥤ E<VAR>K : C ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : D ⥤ E<VAR>R₂ : E ⥤ D<VAR>L₃ : B ⥤ C<VAR>R₃ : C ⥤ B<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : H ⋙ L₄ ⟶ L₃ ⋙ K<VAR>c : C<GOAL>adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))) = adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ ((R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (H.map (adj₁.counit.app (R₃.obj c)))))) ≫ R₂.map (R₄.map (β.app (R₃.obj c)))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G : A ⥤ D<VAR>H : B ⥤ E<VAR>K : C ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : D ⥤ E<VAR>R₂ : E ⥤ D<VAR>L₃ : B ⥤ C<VAR>R₃ : C ⥤ B<VAR>L₄ : E ⥤ F<VAR>R₄ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>adj₄ : L₄ ⊣ R₄<VAR>α : G ⋙ L₂ ⟶ L₁ ⋙ H<VAR>β : H ⋙ L₄ ⟶ L₃ ⋙ K<VAR>c : C<GOAL>adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (L₃.map (adj₁.counit.app (R₃.obj c))))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c))) = adj₂.unit.app (G.obj (R₁.obj (R₃.obj c))) ≫ R₂.map (adj₄.unit.app (L₂.obj (G.obj (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (L₄.map (α.app (R₁.obj (R₃.obj c))))) ≫ R₂.map (R₄.map (β.app (L₁.obj (R₁.obj (R₃.obj c))) ≫ (L₃ ⋙ K).map (adj₁.counit.app (R₃.obj c)))) ≫ R₂.map (R₄.map (K.map (adj₃.counit.app c)))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n m : ℕ<VAR>h : n ≠ m<GOAL>IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n m : ℕ<VAR>h : 0 ≠ m<GOAL>IsCoprime (cyclotomic 0 ℚ) (cyclotomic m ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n m : ℕ<VAR>h : n ≠ m<VAR>hnzero : n > 0<GOAL>IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n : ℕ<VAR>hnzero : n > 0<VAR>h : n ≠ 0<GOAL>IsCoprime (cyclotomic n ℚ) (cyclotomic 0 ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n m : ℕ<VAR>h : n ≠ m<VAR>hnzero : n > 0<VAR>hmzero : m > 0<GOAL>IsCoprime (cyclotomic n ℚ) (cyclotomic m ℚ)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n✝ n m : ℕ<VAR>h : n ≠ m<VAR>hnzero : n > 0<VAR>hmzero : m > 0<GOAL>¬cyclotomic n ℚ ∣ cyclotomic m ℚ
<VAR>a : ℝ<GOAL>closure {z | z.re < a} = {z | z.re ≤ a}
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : FirstCountableTopology X✝<VAR>inst✝ : R1Space X✝<VAR>x y : X✝<VAR>X : Type u_3<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : R1Space X<VAR>h₂ : R1Space X<GOAL>R1Space X
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : FirstCountableTopology X✝<VAR>inst✝ : R1Space X✝<VAR>x y : X✝<VAR>X : Type u_3<VAR>t₁ t₂ : TopologicalSpace X<VAR>h₁ : R1Space X<VAR>h₂ : R1Space X<GOAL>∀ (i : Bool), R1Space X
<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>r : ι → ι → Prop<VAR>inst✝ : IsWellOrder ι r<VAR>o : Ordinal.{u}<VAR>ho : type r = o<VAR>f : (a : Ordinal.{u}) → a < o → α<VAR>i : Ordinal.{u}<VAR>hi : i < o<GOAL>familyOfBFamily' r ho f (enum r i ⋯) = f i hi
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>u u' : Set γ<VAR>v : Set δ<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>d d' : δ<GOAL>image2 f s (t ∪ t') = image2 f s t ∪ image2 f s t'
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.96105, u_1} C<VAR>inst✝² : Category.{?u.96109, u_2} D<VAR>inst✝¹ : Category.{?u.96113, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseLeftKanExtension F<VAR>Y₁ Y₂ : D<VAR>f : Y₁ ⟶ Y₂<VAR>g₁ g₂ : CostructuredArrow L Y₁<VAR>φ : g₁ ⟶ g₂<GOAL>(CostructuredArrow.proj L Y₁ ⋙ F).map φ ≫ (fun g => colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g)) g₂ = (fun g => colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g)) g₁ ≫ ((const (CostructuredArrow L Y₁)).obj (colimit (CostructuredArrow.proj L Y₂ ⋙ F))).map φ