ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f : MultilinearMap R M₁ M₂<VAR>inst✝ : LinearOrder ι<VAR>a b : (i : ι) → M₁ i<VAR>s✝ : Finset ι<VAR>k : ι<VAR>s : Finset ι<VAR>hk : ∀ x ∈ s, k < x<VAR>ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j<GOAL>(f (update (s.piecewise b a) k (s.piecewise b a k - b k)) + ∑ i ∈ s, f fun j => if j ∈ s → j < i then a j else if i = j then a j - b j else b j) = (f fun j => if j = k ∨ j ∈ s → j < k then a j else if k = j then a j - b j else b j) + ∑ x ∈ s, f fun j => if j = k ∨ j ∈ s → j < x then a j else if x = j then a j - b j else b j
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>k✝ : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>k : ℕ<VAR>ih : k ≤ Fintype.card α → ∑ r ∈ range (k + 1), ↑(𝒜 # (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))<VAR>hk : k + 1 ≤ Fintype.card α<GOAL>∑ r ∈ range (k + 1 + 1), ↑(𝒜 # (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(falling (Fintype.card α - (k + 1)) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>k✝ : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>k : ℕ<VAR>ih : k ≤ Fintype.card α → ∑ r ∈ range (k + 1), ↑(𝒜 # (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))<VAR>hk : k + 1 ≤ Fintype.card α<GOAL>↑(𝒜 # (Fintype.card α - (k + 1))).card / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) + ∑ x ∈ range (k + 1), ↑(𝒜 # (Fintype.card α - x)).card / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤ ↑(𝒜 # (Fintype.card α - (k + 1))).card / ↑((Fintype.card α).choose (Fintype.card α - (k + 1))) + ↑(∂ (falling (Fintype.card α - (k + 1) + 1) 𝒜)).card / ↑((Fintype.card α).choose (Fintype.card α - (k + 1)))
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>k✝ : ℕ<VAR>𝒜 : Finset (Finset α)<VAR>s : Finset α<VAR>inst✝ : Fintype α<VAR>h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜<VAR>k : ℕ<VAR>ih : k ≤ Fintype.card α → ∑ r ∈ range (k + 1), ↑(𝒜 # (Fintype.card α - r)).card / ↑((Fintype.card α).choose (Fintype.card α - r)) ≤ ↑(falling (Fintype.card α - k) 𝒜).card / ↑((Fintype.card α).choose (Fintype.card α - k))<VAR>hk : k + 1 ≤ Fintype.card α<GOAL>↑(𝒜 # (Fintype.card α - k - 1)).card / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) + ∑ x ∈ range (k + 1), ↑(𝒜 # (Fintype.card α - x)).card / ↑((Fintype.card α).choose (Fintype.card α - x)) ≤ ↑(𝒜 # (Fintype.card α - k - 1)).card / ↑((Fintype.card α).choose (Fintype.card α - k - 1)) + ↑(∂ (falling (Fintype.card α - k) 𝒜)).card / ↑((Fintype.card α).choose (Fintype.card α - k - 1))
<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<GOAL>IsClosed {p | p.1 ⤳ p.2}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<GOAL>∃ s, Nonempty (α ≃ᵐ ↑s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<GOAL>Measurable ⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<GOAL>∀ t ∈ range (natGeneratingSequence α), MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>n : ℕ<GOAL>MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯).symm ⁻¹' natGeneratingSequence α n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>n : ℕ<GOAL>MeasurableSet (⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>n : ℕ<GOAL>Subtype.val ⁻¹' {y | y n = true} = ⇑(Equiv.ofInjective (mapNatBool α) ⋯) '' natGeneratingSequence α n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>n : ℕ<GOAL>⇑(Equiv.ofInjective (mapNatBool α) ⋯) ⁻¹' (Subtype.val ⁻¹' {y | y n = true}) = natGeneratingSequence α n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)<GOAL>∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>κ : Kernel α (β × Ω)<VAR>inst✝ : IsFiniteKernel κ<VAR>f : β × Ω → ℝ≥0∞<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set Ω<VAR>ht : MeasurableSet t<VAR>this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)<GOAL>∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a
<VAR>a✝¹ a✝ : ℕ<GOAL>↑a✝¹ + ↑a✝ = 2 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 2 ∨ ↑a✝¹ = 1 ∧ ↑a✝ = 1 ∨ ↑a✝¹ = 2 ∧ ↑a✝ = 0
<VAR>a : ONote<VAR>m : ℕ+<VAR>b : ONote<VAR>iha : a.FundamentalSequenceProp a.fundamentalSequence<VAR>ihb : b.FundamentalSequenceProp b.fundamentalSequence<GOAL>(a.oadd m b).FundamentalSequenceProp (match b.fundamentalSequence with | Sum.inr f => Sum.inr fun i => a.oadd m (f i) | Sum.inl (some b') => Sum.inl (some (a.oadd m b')) | Sum.inl none => match a.fundamentalSequence, m.natPred with | Sum.inl none, 0 => Sum.inl (some zero) | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero)) | Sum.inl (some a'), 0 => Sum.inr fun i => a'.oadd i.succPNat zero | Sum.inl (some a'), m.succ => Sum.inr fun i => a.oadd m.succPNat (a'.oadd i.succPNat zero) | Sum.inr f, 0 => Sum.inr fun i => (f i).oadd 1 zero | Sum.inr f, m.succ => Sum.inr fun i => a.oadd m.succPNat ((f i).oadd 1 zero))
<VAR>a : ONote<VAR>m : ℕ+<VAR>b : ONote<VAR>iha : a.FundamentalSequenceProp a.fundamentalSequence<VAR>ihb : b = 0<VAR>e : b.fundamentalSequence = Sum.inl none<GOAL>match match a.fundamentalSequence, m.natPred with | Sum.inl none, 0 => Sum.inl (some zero) | Sum.inl none, m.succ => Sum.inl (some (zero.oadd m.succPNat zero)) | Sum.inl (some a'), 0 => Sum.inr fun i => a'.oadd i.succPNat zero | Sum.inl (some a'), m.succ => Sum.inr fun i => a.oadd m.succPNat (a'.oadd i.succPNat zero) | Sum.inr f, 0 => Sum.inr fun i => (f i).oadd 1 zero | Sum.inr f, m.succ => Sum.inr fun i => a.oadd m.succPNat ((f i).oadd 1 zero) with | Sum.inl none => a.oadd m b = 0 | Sum.inl (some a_1) => (a.oadd m b).repr = succ a_1.repr ∧ ((a.oadd m b).NF → a_1.NF) | Sum.inr f => (a.oadd m b).repr.IsLimit ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a.oadd m b ∧ ((a.oadd m b).NF → (f i).NF)) ∧ ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (f i).repr
<VAR>a : ONote<VAR>m : ℕ+<VAR>b : ONote<VAR>iha : a.FundamentalSequenceProp a.fundamentalSequence<VAR>b' : ONote<VAR>ihb : b.repr = succ b'.repr ∧ (b.NF → b'.NF)<VAR>e : b.fundamentalSequence = Sum.inl (some b')<GOAL>(a.oadd m b).repr = succ (a.oadd m b').repr ∧ ((a.oadd m b).NF → (a.oadd m b').NF)
<VAR>a : ONote<VAR>m : ℕ+<VAR>b : ONote<VAR>iha : a.FundamentalSequenceProp a.fundamentalSequence<VAR>f : ℕ → ONote<VAR>ihb : b.repr.IsLimit ∧ (∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)) ∧ ∀ a < b.repr, ∃ i, a < (f i).repr<VAR>e : b.fundamentalSequence = Sum.inr f<GOAL>(a.oadd m b).repr.IsLimit ∧ (∀ (i : ℕ), a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧ ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m (f i)).repr
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module.Free R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : IsKilling R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>I : LieIdeal R L<VAR>inst✝ : IsLieAbelian ↥↑I<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : LieAlgebra K L<VAR>inst✝⁵ : Module.Free R L<VAR>inst✝⁴ : Module.Finite R L<VAR>inst✝³ : IsKilling R L<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsPrincipalIdealRing R<VAR>I : LieIdeal R L<VAR>inst✝ : IsLieAbelian ↥↑I<GOAL>I ≤ LieIdeal.killingCompl R L ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r f : R[X]<VAR>a : R<GOAL>f.natDegree + (C a).natDegree = f.natDegree + 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<GOAL>UniformConcaveOn s φ (-f)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a✝ b✝ m : ℝ<VAR>x✝ y✝ : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>-(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι), IsCompact (s i)<GOAL>IsCompact (univ.pi s)
<VAR>X✝ : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X✝<VAR>X : ι → Type u_2<VAR>inst✝ : (i : ι) → TopologicalSpace (X i)<VAR>s : (i : ι) → Set (X i)<VAR>h : ∀ (i : ι), IsCompact (s i)<GOAL>univ.pi s = {x | ∀ (i : ι), x i ∈ s i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : T1Space E<VAR>hxy : x ≠ y<GOAL>∃ f, f x < f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : ContinuousSMul ℝ E<VAR>s✝ t✝ : Set E<VAR>x y : E<VAR>inst✝¹ : LocallyConvexSpace ℝ E<VAR>inst✝ : T1Space E<VAR>hxy : x ≠ y<VAR>f : E →L[ℝ] ℝ<VAR>s t : ℝ<VAR>hs : ∀ a ∈ {x}, f a < s<VAR>st : s < t<VAR>ht : ∀ b ∈ {y}, t < f b<GOAL>∃ f, f x < f y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>M₁ M₂ : Matroid α<VAR>hE : M₁.E = M₂.E<VAR>h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B)<GOAL>M₁ = M₂
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>M₁ M₂ : Matroid α<VAR>hE : M₁.E = M₂.E<VAR>h : ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.Base B ↔ M₂.Base B)<VAR>h' : ∀ (B : Set α), M₁.Base B ↔ M₂.Base B<GOAL>M₁ = M₂
<VAR>a x✝ z x : ℂ<GOAL>↑((starRingEnd ℂ) x).arg = -↑x.arg
<VAR>R : Type u_1<VAR>inst✝¹⁴ : Semiring R<VAR>M : Type u_2<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : Module R M<VAR>N : Type u_3<VAR>inst✝¹¹ : AddCommMonoid N<VAR>inst✝¹⁰ : Module R N<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommMonoid P<VAR>inst✝⁸ : Module R P<VAR>M' : Type u_5<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : Module R M'<VAR>N' : Type u_6<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>N'₂ : Type u_10<VAR>inst✝³ : AddCommGroup N'₂<VAR>inst✝² : Module R N'₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>g : N' →ₗ[R] N'₂<VAR>f : MultilinearMap R (fun x => M) N'<VAR>x✝ : ι → M<GOAL>(MultilinearMap.alternatization (g.compMultilinearMap f)) x✝ = (g.compAlternatingMap (MultilinearMap.alternatization f)) x✝
<VAR>α : Type u<VAR>n : ℕ<VAR>f : Fin n → α<VAR>h : ofFn f ≠ []<VAR>hn : optParam (n - 1 < n) ⋯<GOAL>(ofFn f).getLast h = f ⟨n - 1, hn⟩
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝¹ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝¹ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝¹ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝¹ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝² : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝² : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<GOAL>Nonempty (IsColimit c')
<VAR>J : Type v'<VAR>inst✝⁷ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝⁵ : Category.{?u.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝² : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<GOAL>Nonempty (IsColimit c')