ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p b : α<VAR>hp : p ≠ 0<VAR>a : αˣ<VAR>ha : p * b * ↑a = p<GOAL>IsUnit b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p b : α<VAR>hp : p ≠ 0<VAR>a : αˣ<VAR>ha : p * b * ↑a = p<GOAL>p * (b * ↑a) = p * 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₀₁.τ₂ ≫ S.v₁₂.τ₂ = 0
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Set (Subalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.33393, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>((Cochain.ofHom (inr φ)).comp ↑(fst φ) ⋯).v p q hpq = Cochain.v 0 p q hpq
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>h : ⊥.jacobson = ⊥<GOAL>⊥.jacobson = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>h : ⊥.jacobson = ⊥<GOAL>sInf (map C '' {J | J.IsMaximal}) ≤ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>h : ⊥.jacobson = ⊥<VAR>f : R[X]<VAR>hf : f ∈ sInf (map C '' {J | J.IsMaximal})<VAR>n : ℕ<GOAL>f.coeff n = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>h : ⊥.jacobson = ⊥<VAR>f : R[X]<VAR>hf : f ∈ sInf (map C '' {J | J.IsMaximal})<VAR>n : ℕ<GOAL>f.coeff n ∈ ⊥.jacobson
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝³ : TotalComplexShape c₂ c₁ c₁₂<VAR>inst✝² : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>inst✝¹ : TotalComplexShapeSymmetry c₂ c₁ c₁₂<VAR>inst✝ : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂<VAR>i₁ : I₁<VAR>i₂ : I₂<GOAL>c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>I : Ideal R<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>map f I = ⊥ ↔ I = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>c₁ c₂ : R<VAR>q : Basis A c₁ c₂<GOAL>q.k * q.j = c₂ • q.i
<VAR>C : Type u_1<VAR>inst✝ : Groupoid C<VAR>h : ∀ (c : C), Subsingleton (c ⟶ c)<VAR>c d : C<VAR>f g : c ⟶ d<VAR>this : Subsingleton (d ⟶ d)<GOAL>f = g
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₁, u₁} C<VAR>inst✝¹¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹⁰ : Category.{v₃, u₃} E<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝⁹ : L.IsLocalization W<VAR>A : Type w<VAR>inst✝⁸ : AddMonoid A<VAR>inst✝⁷ : HasShift C A<VAR>inst✝⁶ : W.IsCompatibleWithShift A<VAR>inst✝⁵ : W.HasLocalization<VAR>F : C ⥤ E<VAR>F' : D ⥤ E<VAR>inst✝⁴ : Lifting L W F F'<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : L.CommShift A<VAR>inst✝ : F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(F'.commShiftIso a).hom.app (L.obj X) = F'.map ((L.commShiftIso a).inv.app X) ≫ (Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X) ≫ (F.commShiftIso a).hom.app X ≫ (shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>hf : Partrec' f<VAR>v : Vector ℕ n.succ<GOAL>f (ofFn fun i => v.get i.succ) = f v.tail
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>hf : Partrec' f<VAR>v : Vector ℕ n.succ<GOAL>f (ofFn fun i => v.get i.succ) = f (ofFn v.tail.get)
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>hf : Partrec' f<VAR>v : Vector ℕ n.succ<GOAL>(fun i => v.get i.succ) = v.tail.get
<VAR>n : ℕ<VAR>f : Vector ℕ n →. ℕ<VAR>hf : Partrec' f<VAR>v : Vector ℕ n.succ<VAR>i : Fin n<GOAL>v.get i.succ = v.tail.get i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionMonoid K<VAR>inst✝ : HasDistribNeg K<VAR>a b : K<GOAL>(-1)⁻¹ = -1
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : Field 𝕜<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq p<VAR>inst✝¹ : CommRing R<VAR>i j : n<VAR>inst✝ : Fintype n<VAR>i✝ j✝ : n<VAR>t_hij : i✝ ≠ j✝<VAR>c✝ : R<GOAL>{ i := i✝, j := j✝, hij := t_hij, c := c✝ }.inv.toMatrix * { i := i✝, j := j✝, hij := t_hij, c := c✝ }.toMatrix = 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
<VAR>S : Finset Λ'<VAR>q : Λ'<VAR>H₁ : Λ'.Supports S q<VAR>HS₁ : trStmts₁ q ⊆ S<GOAL>Supports (trStmts₁ q) S
<VAR>S : Finset Λ'<VAR>q : Λ'<VAR>H₁ : Λ'.Supports S q<VAR>HS₁ : trStmts₁ q ⊆ S<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<GOAL>Supports (trStmts₁ q) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>p✝ : Γ' → Bool<VAR>k₁✝ k₂✝ : K'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)<VAR>HS₁ : insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q) ⊆ S<GOAL>Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>p✝ : Γ' → Bool<VAR>k✝ : K'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)<VAR>HS₁ : insert (Λ'.clear p✝ k✝ q) (trStmts₁ q) ⊆ S<GOAL>Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S q.copy<VAR>HS₁ : insert q.copy (trStmts₁ q) ⊆ S<GOAL>Supports (insert q.copy (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>k✝ : K'<VAR>s✝ : Option Γ' → Option Γ'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)<VAR>HS₁ : insert (Λ'.push k✝ s✝ q) (trStmts₁ q) ⊆ S<GOAL>Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Option Γ' → Λ'<VAR>q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S<VAR>H₁ : Λ'.Supports S (Λ'.read q)<VAR>HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s)) ⊆ S<GOAL>Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S q.succ<VAR>HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S<GOAL>Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q₁ q₂ : Λ'<VAR>q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S<VAR>q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S<VAR>H₁ : Λ'.Supports S (q₁.pred q₂)<VAR>HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S<GOAL>Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>k✝ : Cont'<VAR>H₁ : Λ'.Supports S (Λ'.ret k✝)<VAR>HS₁ : {Λ'.ret k✝} ⊆ S<GOAL>Supports {Λ'.ret k✝} S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>p✝ : Γ' → Bool<VAR>k₁✝ k₂✝ : K'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.move p✝ k₁✝ k₂✝ q)<VAR>HS₁ : insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q) ⊆ S<VAR>h₁ : Λ'.move p✝ k₁✝ k₂✝ q ∈ S<VAR>h₂ : trStmts₁ q ⊆ S<VAR>h₃ : q ∈ S<GOAL>Supports (insert (Λ'.move p✝ k₁✝ k₂✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>p✝ : Γ' → Bool<VAR>k✝ : K'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.clear p✝ k✝ q)<VAR>HS₁ : insert (Λ'.clear p✝ k✝ q) (trStmts₁ q) ⊆ S<VAR>h₁ : Λ'.clear p✝ k✝ q ∈ S<VAR>h₂ : trStmts₁ q ⊆ S<VAR>h₃ : q ∈ S<GOAL>Supports (insert (Λ'.clear p✝ k✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S q.copy<VAR>HS₁ : insert q.copy (trStmts₁ q) ⊆ S<VAR>h₁ : q.copy ∈ S<VAR>h₂ : trStmts₁ q ⊆ S<VAR>h₃ : q ∈ S<GOAL>Supports (insert q.copy (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>k✝ : K'<VAR>s✝ : Option Γ' → Option Γ'<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S (Λ'.push k✝ s✝ q)<VAR>HS₁ : insert (Λ'.push k✝ s✝ q) (trStmts₁ q) ⊆ S<VAR>h₁ : Λ'.push k✝ s✝ q ∈ S<VAR>h₂ : trStmts₁ q ⊆ S<VAR>h₃ : q ∈ S<GOAL>Supports (insert (Λ'.push k✝ s✝ q) (trStmts₁ q)) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Option Γ' → Λ'<VAR>q_ih : ∀ (a : Option Γ'), Λ'.Supports S (q a) → trStmts₁ (q a) ⊆ S → Supports (trStmts₁ (q a)) S<VAR>H₁ : Λ'.Supports S (Λ'.read q)<VAR>HS₁ : insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s)) ⊆ S<VAR>h₁ : Λ'.read q ∈ S<VAR>h₂ : ∀ ⦃x : Λ'⦄ (x_1 : Option Γ'), x ∈ trStmts₁ (q x_1) → x ∈ S<GOAL>Supports (insert (Λ'.read q) (Finset.univ.biUnion fun s => trStmts₁ (q s))) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q : Λ'<VAR>q_ih : Λ'.Supports S q → trStmts₁ q ⊆ S → Supports (trStmts₁ q) S<VAR>H₁ : Λ'.Supports S q.succ<VAR>HS₁ : insert q.succ (insert (unrev q) (trStmts₁ q)) ⊆ S<VAR>h₁ : q.succ ∈ S<VAR>h₂ : unrev q ∈ S ∧ ∀ a ∈ trStmts₁ q, a ∈ S<GOAL>Supports (insert q.succ (insert (unrev q) (trStmts₁ q))) S
<VAR>S : Finset Λ'<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<VAR>q₁ q₂ : Λ'<VAR>q₁_ih : Λ'.Supports S q₁ → trStmts₁ q₁ ⊆ S → Supports (trStmts₁ q₁) S<VAR>q₂_ih : Λ'.Supports S q₂ → trStmts₁ q₂ ⊆ S → Supports (trStmts₁ q₂) S<VAR>H₁ : Λ'.Supports S (q₁.pred q₂)<VAR>HS₁ : insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂)) ⊆ S<VAR>h₁ : q₁.pred q₂ ∈ S<VAR>h₂ : unrev q₂ ∈ S ∧ ∀ (a : Λ'), a ∈ trStmts₁ q₁ ∨ a ∈ trStmts₁ q₂ → a ∈ S<GOAL>Supports (insert (q₁.pred q₂) (insert (unrev q₂) (trStmts₁ q₁ ∪ trStmts₁ q₂))) S
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MulZeroClass G₀<VAR>a : G₀<GOAL>SemiconjBy a 0 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>κ : Sort u_5<VAR>s : κ → HomogeneousIdeal 𝒜<GOAL>(⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>span R s = ⨆ x ∈ s, span R {x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring R₂<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_5<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f g : F<GOAL>eqLocus f g = ⊤ ↔ f = g
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>R : ℝ<GOAL>∫ (x : E), f (R⁻¹ • x) ∂μ = |R ^ finrank ℝ E| • ∫ (x : E), f x ∂μ
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<GOAL>IsSheafFor F (ofArrows X c.inj)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<GOAL>∀ (y : Equalizer.Presieve.Arrows.FirstObj F X), Equalizer.Presieve.Arrows.firstMap F X c.inj y = Equalizer.Presieve.Arrows.secondMap F X c.inj y → ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : IsIso (piComparison F fun x => op (X x))<GOAL>∀ (y : Equalizer.Presieve.Arrows.FirstObj F X), Equalizer.Presieve.Arrows.firstMap F X c.inj y = Equalizer.Presieve.Arrows.secondMap F X c.inj y → ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<GOAL>∀ (y : Equalizer.Presieve.Arrows.FirstObj F X), Equalizer.Presieve.Arrows.firstMap F X c.inj y = Equalizer.Presieve.Arrows.secondMap F X c.inj y → ∃! x, Equalizer.Presieve.Arrows.forkMap F X c.inj x = y
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>y = F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom y = F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv t)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom y = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>𝟙 (F.obj (∏ᶜ fun x => op (X x))) t = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>F.map (𝟙 (∏ᶜ fun x => op (X x))) t = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom) t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>F.map (𝟙 (∏ᶜ fun x => op (X x))) = F.map ((opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom)