ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormalSpace Y<VAR>inst✝ : Nonempty X<VAR>f : X →ᵇ ℝ<VAR>e : X → Y<VAR>he : ClosedEmbedding e<VAR>inhabited_h : Inhabited X<VAR>a : ℝ<VAR>ha : IsGLB (range ⇑f) a<VAR>b : ℝ<VAR>hb : IsLUB (range ⇑f) b<VAR>hmem : ∀ (x : X), f x ∈ Icc a b<VAR>hle : a ≤ b<VAR>hlt : a < b<VAR>c : ℝ := (a + b) / 2<VAR>hac : a < c<VAR>hcb : c < b<VAR>hsub : c - a = b - c<VAR>g : Y →ᵇ ℝ<VAR>xl : Y → X<VAR>hxl : ∀ (y : Y), f (xl y) ≤ g y<VAR>hgb : ∀ (y : Y), g y ≤ b<VAR>hb' : ¬∃ x, f x = b<VAR>hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})<VAR>dg : Y →ᵇ ℝ<VAR>dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)<VAR>dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})<VAR>dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)<VAR>hgf : ∀ (x : X), (g - dg) (e x) = f x<VAR>y : Y<VAR>hyb : (g - dg) y < b<VAR>xu : X<VAR>hyxu : (g - dg) y < f xu<VAR>right✝ : f xu ≤ b<VAR>hc : g y ≤ c<GOAL>∃ x₁ x₂, (g - dg) y ∈ Icc (f x₁) (f x₂)
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Pow M ℕ+<VAR>inst✝ : PNatPowAssoc M<VAR>m n : ℕ+<VAR>x : M<GOAL>x ^ m * x ^ n = x ^ n * x ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : ι → Set α<VAR>x : β<GOAL>x ∈ f '' ⋃ i, s i ↔ x ∈ ⋃ i, f '' s i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : ι → Set α<VAR>x : β<GOAL>(∃ x_1 x_2, x_1 ∈ s x_2 ∧ f x_1 = x) ↔ ∃ i, ∃ x_1 ∈ s i, f x_1 = x
<VAR>n m b : ℕ<GOAL>m < (b + 1 + 1) ^ ((b + 1 + 1).digits m).length
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>inst✝² : Nonempty β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : NoMaxOrder β<VAR>u : β → α<VAR>a : α<GOAL>(∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ioi ia, u x ∈ ball a ib) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A✝ B X✝ X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A✝<VAR>A X : C<VAR>inst✝ : Exponentiable A<GOAL>curry (𝟙 (A ⨯ (𝟭 C).obj X)) = (exp.coev A).app X
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>A✝ B X✝ X' Y Y' Z : C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : Exponentiable A✝<VAR>A X : C<VAR>inst✝ : Exponentiable A<GOAL>(exp.coev A).app ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⨯ (𝟭 C).obj X) = (exp.coev A).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasFiniteProducts C<VAR>inst✝ : HasPullbacks C<VAR>X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>g₁ : Y₁ ⟶ Z₁<VAR>g₂ : Y₂ ⟶ Z₂<GOAL>π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F, prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) = π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.IsReflection (cs.simple i)
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<GOAL>cs.simple i = 1 * cs.simple i * 1⁻¹
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<VAR>f : P →ᵃ[R] P'<VAR>hf : Injective ⇑f<GOAL>Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>J : GrothendieckTopology C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : HasWeakSheafify J D<VAR>T : C<VAR>hT : IsTerminal T<VAR>F : Sheaf J D<GOAL>(constantSheafAdj J D hT).counit.app F = (presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val) ≫ (sheafificationAdjunction J D).counit.app F
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>J : GrothendieckTopology C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : HasWeakSheafify J D<VAR>T : C<VAR>hT : IsTerminal T<VAR>F : Sheaf J D<GOAL>((constantSheafAdj J D hT).counit.app F).val = ((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val) ≫ (sheafificationAdjunction J D).counit.app F).val
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>J : GrothendieckTopology C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : HasWeakSheafify J D<VAR>T : C<VAR>hT : IsTerminal T<VAR>F : Sheaf J D<GOAL>toSheafify J ((const Cᵒᵖ).obj (((sheafSections J D).obj (op T)).obj F)) ≫ ((constantSheafAdj J D hT).counit.app F).val = toSheafify J ((const Cᵒᵖ).obj (((sheafSections J D).obj (op T)).obj F)) ≫ ((presheafToSheaf J D).map ((constantPresheafAdj D hT).counit.app F.val) ≫ (sheafificationAdjunction J D).counit.app F).val
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>J : GrothendieckTopology C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>inst✝ : HasWeakSheafify J D<VAR>T : C<VAR>hT : IsTerminal T<VAR>F : Sheaf J D<GOAL>toSheafify J ((const Cᵒᵖ).obj (F.val.obj (op T))) ≫ 𝟙 ((presheafToSheaf J D).obj ((const Cᵒᵖ).obj (F.val.obj (op T)))).val ≫ sheafifyLift J { app := fun x => F.val.map (hT.from (unop x)).op, naturality := ⋯ } ⋯ = { app := fun x => F.val.map (hT.from (unop x)).op, naturality := ⋯ }
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝ : LinearOrder α<VAR>a : α<GOAL>Bounded (fun x x_1 => x ≤ x_1) (s ∩ {b | a < b}) ↔ Bounded (fun x x_1 => x ≤ x_1) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>p : ExactPairing X Y<GOAL>(leftDualIso p p).hom = (Iso.refl X).hom
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>c : ℂ<VAR>R : ℝ<VAR>hR : R ≠ 0<GOAL>(∮ (z : ℂ) in C(c, R), (z - c)⁻¹) = 2 * ↑π * I
<VAR>α : Type u_1<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PredOrder α<VAR>inst✝ : NoMinOrder α<VAR>b : α<VAR>h : IsPredLimit (pred b)<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>XYIdeal W x (C (W.negY x y)) * XYIdeal W x (C y) = XIdeal W x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>XYIdeal W x (C (W.negY x y)) * XYIdeal W x (C y) = XIdeal W x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>span {(mk W) (C (X - C x))} * span {(mk W) (C (X - C x)), (mk W) (Y - C (C y)), (mk W) (Y - C (C (W.negY x y))), (AdjoinRoot.mk W.polynomial) (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)} = XIdeal W x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>span {(mk W) (C (X - C x)), (mk W) (Y - C (C y)), (mk W) (Y - C (C (W.negY x y))), (AdjoinRoot.mk W.polynomial) (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y)} = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>Ideal.map (mk W) (span {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)), C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y}) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>Ideal.map (mk W) (span {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)), C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y}) = Ideal.map (mk W) ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>span {C (X - C x), Y - C (C y), Y - C (C (W.negY x y)), C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y} = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<GOAL>∃ a a_1 a_2 a_3, a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = 1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<VAR>hx : W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0<GOAL>∃ a a_1 a_2 a_3, a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = 1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<VAR>Y_rw : (Y - C (C y)) * (Y - C (C (W.negY x y))) - C (X - C x) * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = W.polynomial * 1<VAR>hy : 2 * y + W.a₁ * x + W.a₃ ≠ 0<GOAL>∃ a a_1 a_2 a_3, a_3 * (C (X ^ 2 + C (x + W.a₂) * X + C (x ^ 2 + W.a₂ * x + W.a₄)) - C (C W.a₁) * Y) = 1 + a * C (X - C x) + a_1 * (Y - C (C y)) + a_2 * (Y - C (C (W.negY x y)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>n : ℕ<GOAL>a ^ (n + 1) ≤ a∗
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : KleeneAlgebra α<VAR>a b c : α<VAR>n : ℕ<GOAL>a * a ^ n ≤ a∗
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>t₁' : Nonempty (IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>j : Fin n<GOAL>(α.app { as := j.succ } ≫ c₁.inj j) ≫ c₂.inr = c.ι.app { as := j.succ } ≫ i
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<GOAL>(Discrete.natTrans fun i => α.app { as := i.as.succ }) ≫ c₁.ι = (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯).ι ≫ (Functor.const (Discrete (Fin n))).map (pullback.fst c₂.inr i)
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<GOAL>∀ (j : Discrete (Fin n)), IsPullback ((Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯).ι.app j) ((Discrete.natTrans fun i => α.app { as := i.as.succ }).app j) (pullback.fst c₂.inr i) (c₁.ι.app j)
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<VAR>t₂' : Nonempty (IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)))<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<GOAL>mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι = (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (Functor.const (Discrete WalkingPair)).map i
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk<VAR>this : F = Discrete.functor F'<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<GOAL>∀ (j : Discrete WalkingPair), IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι.app j) ((mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)).app j) i (c₂.ι.app j)
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F' : Fin (n + 1) → C<VAR>c : Cocone (Discrete.functor F')<VAR>α : Discrete.functor F' ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<VAR>H₂ : IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i))<VAR>j : Fin (n + 1)<GOAL>Fin.cases (c.ι.app { as := 0 }) (fun i_1 => pullback.lift (α.app { as := i_1.succ } ≫ c₁.inj i_1) (c.ι.app { as := i_1.succ }) ⋯ ≫ pullback.snd c₂.inr i) { as := j }.as ≫ 𝟙 c.pt = c.ι.app { as := j }
<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.288379, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.288386, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsUniversalColimit c₁<VAR>t₂ : IsUniversalColimit c₂<VAR>inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>F' : Fin (n + 1) → C<VAR>c : Cocone (Discrete.functor F')<VAR>α : Discrete.functor F' ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)<VAR>H₁ : IsColimit (Cofan.mk (pullback c₂.inr i) fun j => pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)<VAR>H₂ : IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i))<VAR>j : Fin (n + 1)<GOAL>Fin.cases (c.ι.app { as := 0 }) (fun i => c.ι.app { as := i.succ }) j = c.ι.app { as := j }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : NoZeroDivisors A<VAR>x : A<VAR>hx : x ≠ 0<VAR>this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }<GOAL>Function.Injective ⇑((mul R A) x)