ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>U : Y.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X.Hom Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : X.Opens<GOAL>AlgebraicGeometry.IsAffineOpen (f.opensFunctor.obj U) ↔ AlgebraicGeometry.IsAffineOpen U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : ↑X.affineOpens<GOAL>↑↑((AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv f) U) = (AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj ↑U
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>H : AlgebraicGeometry.IsOpenImmersion f<VAR>U : { U // ↑U ≤ AlgebraicGeometry.Scheme.Hom.opensRange f }<GOAL>↑((AlgebraicGeometry.IsOpenImmersion.affineOpensEquiv f).symm U) = (TopologicalSpace.Opens.map f.val.base).obj ↑↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<GOAL>∀ (a : ↑(↑U).affineOpens), ↑↑((AlgebraicGeometry.affineOpensRestrict U) a) = (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj ↑a
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>V : { V // ↑V ≤ U }<GOAL>↑((AlgebraicGeometry.affineOpensRestrict U).symm V) = (TopologicalSpace.Opens.map U.ι.val.base).obj ↑↑V
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>(TopologicalSpace.Opens.map hU.fromSpec.val.base).obj U = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>(AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom ≫ AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U = (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<GOAL>AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U = (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv ≫ (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).inv f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(TopologicalSpace.Opens.map hU.fromSpec.val.base).obj (X.basicOpen f) = PrimeSpectrum.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Scheme.Hom.opensFunctor hU.fromSpec).obj (PrimeSpectrum.basicOpen f) = X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>(AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).basicOpen ((AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U) f) = PrimeSpectrum.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>AlgebraicGeometry.IsAffineOpen (X.basicOpen f)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>r : ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map (X.basicOpen r).ι.val.base).obj U)
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>V : X.Opens<VAR>x : ↥V<VAR>h : ↑x ∈ U<GOAL>∃ f, X.basicOpen f ≤ V ∧ ↑x ∈ X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<GOAL>IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>V : X.Opens<VAR>hV : AlgebraicGeometry.IsAffineOpen V<VAR>e : V ≤ (TopologicalSpace.Opens.map f.val.base).obj U<VAR>r : ↑(Y.presheaf.obj (Opposite.op U))<GOAL>AlgebraicGeometry.Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) r)) ⋯ = IsLocalization.Away.map (↑(Y.presheaf.obj (Opposite.op (Y.basicOpen r)))) (↑(X.presheaf.obj (Opposite.op (X.basicOpen ((AlgebraicGeometry.Scheme.Hom.appLE f U V e) r))))) (AlgebraicGeometry.Scheme.Hom.appLE f U V e) r
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>V : X.Opens<VAR>i : V ⟶ U<VAR>e : V = X.basicOpen f<GOAL>IsLocalization.Away f ↑(X.presheaf.obj (Opposite.op V))
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : ↑(X.presheaf.obj (Opposite.op U))<VAR>g : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))<GOAL>∃ f', X.basicOpen f' = X.basicOpen g
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>V : X.Opens<VAR>hV : AlgebraicGeometry.IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>x : ↥U<GOAL>hU.fromSpec.val.base (hU.primeIdealOf x) = ↑x
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>y : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))<VAR>hy : hU.fromSpec.val.base y ∈ U<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec.val.base y))) y.asIdeal
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>x : ↥U<GOAL>IsLocalization.AtPrime (↑(X.presheaf.stalk ↑x)) (hU.primeIdealOf x).asIdeal
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : ↑X.affineOpens<VAR>f : ↑(X.presheaf.obj (Opposite.op ↑U))<GOAL>↑(X.affineBasicOpen f) = X.basicOpen f
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<GOAL>⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<GOAL>U ≤ ⨆ f, X.basicOpen ↑f ↔ Ideal.span s = ⊤
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<VAR>hs : Ideal.span s = ⊤<GOAL>⨆ i ∈ s, X.basicOpen i = U
<VAR>X : AlgebraicGeometry.Scheme<VAR>P : ↑X.affineOpens → Prop<VAR>ι : Sort u_2<VAR>U : ι → ↑X.affineOpens<VAR>iSup_U : ⨆ i, ↑(U i) = ⊤<VAR>V : ↑X.affineOpens<VAR>basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), P U → P (X.affineBasicOpen f)<VAR>openCover : ∀ (U : ↑X.affineOpens) (s : Finset ↑(X.presheaf.obj (Opposite.op ↑U))), Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U<VAR>hU : ∀ (i : ι), P (U i)<GOAL>P V
<VAR>X : AlgebraicGeometry.Scheme<VAR>s : Set ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>⇑(AlgebraicGeometry.ΓSpec.adjunction.unit.app X).val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>s : Set ↑(X.presheaf.obj (Opposite.op ⊤))<GOAL>⇑X.isoSpec.hom.val.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>s : Set ↑↑X.toPresheafedSpace<GOAL>IsClosed s ↔ ∃ I, s = X.zeroLocus ↑I
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>p : PrimeSpectrum ↑S<GOAL>(AlgebraicGeometry.StructureSheaf.stalkIso (↑R) ((PrimeSpectrum.comap f) p)).hom ≫ CommRingCat.ofHom (Localization.localRingHom ((PrimeSpectrum.comap f) p).asIdeal p.asIdeal f ⋯) ≫ (AlgebraicGeometry.StructureSheaf.stalkIso (↑S) p).inv = AlgebraicGeometry.Scheme.Hom.stalkMap (AlgebraicGeometry.Spec.map f) p
<VAR>self : AlgebraicGeometry.Scheme.GlueData<VAR>i j : self.J<GOAL>AlgebraicGeometry.IsOpenImmersion (self.f i j)
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i : D.J<GOAL>D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv = D.ι i
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>x : ↑↑D.glued.toPresheafedSpace<GOAL>∃ i y, (D.ι i).val.base y = x
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i j : D.J<GOAL>D.t i j ≫ D.f j i ≫ D.ι j = D.f i j ≫ D.ι i
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i : D.J<GOAL>D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫ D.isoCarrier.inv = (D.ι i).val.base
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i j : D.J<VAR>x : ↑↑(D.U i).toPresheafedSpace<VAR>y : ↑↑(D.U j).toPresheafedSpace<GOAL>(D.ι i).val.base x = (D.ι j).val.base y ↔ D.Rel ⟨i, x⟩ ⟨j, y⟩
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>U : Set ↑↑D.glued.toPresheafedSpace<GOAL>IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(D.ι i).val.base ⁻¹' U)
<VAR>D : AlgebraicGeometry.Scheme.GlueData<GOAL>∀ (a : D.J), D.openCover.obj a = D.U a
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i : D.J<GOAL>D.openCover.map i = D.ι i
<VAR>D : AlgebraicGeometry.Scheme.GlueData<GOAL>D.openCover.J = D.J
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>x : ↑↑D.glued.toPresheafedSpace<GOAL>D.openCover.f x = ⋯.choose
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x)) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x)) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map z) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map z)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x)) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map z)) (CategoryTheory.Limits.pullback.fst (𝒰.map y) (𝒰.map x)) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map y) (𝒰.map x) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z))
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y = 𝟙 (CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)) (CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map z)))
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>∀ (x : 𝒰.J × 𝒰.J), 𝒰.gluedCover.V x = match x with | (x, y) => CategoryTheory.Limits.pullback (𝒰.map x) (𝒰.map y)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y : 𝒰.J<GOAL>𝒰.gluedCover.t x y = (CategoryTheory.Limits.pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>𝒰.gluedCover.J = 𝒰.J
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCover.t' x y z = 𝒰.gluedCoverT' x y z
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x y : 𝒰.J<GOAL>𝒰.gluedCover.f x y = CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y)
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>∀ (a : 𝒰.J), 𝒰.gluedCover.U a = 𝒰.obj a
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>x : 𝒰.J<GOAL>𝒰.gluedCover.ι x ≫ 𝒰.fromGlued = 𝒰.map x
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>Function.Injective ⇑𝒰.fromGlued.val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>IsOpenMap ⇑𝒰.fromGlued.val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>OpenEmbedding ⇑𝒰.fromGlued.val.base
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : AlgebraicGeometry.Scheme<VAR>f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y<VAR>hf : ∀ (x y : 𝒰.J), CategoryTheory.Limits.pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = CategoryTheory.Limits.pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y<VAR>x : 𝒰.J<GOAL>𝒰.map x ≫ 𝒰.glueMorphisms f hf = f x
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>Y : AlgebraicGeometry.Scheme<VAR>f₁ f₂ : X ⟶ Y<VAR>h : ∀ (x : 𝒰.J), 𝒰.map x ≫ f₁ = 𝒰.map x ≫ f₂<GOAL>f₁ = f₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : α ⊕ β → Sort u_3<VAR>p : ((ab : α ⊕ β) → γ ab) → Prop<GOAL>(∃ fab, p fab) ↔ ∃ fa fb, p fun t => Sum.rec fa fb t
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.Injective Sum.inl
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.Injective Sum.inr
<VAR>α : Type u<VAR>β : Type v<VAR>P : α ⊕ β → Sort u_3<VAR>f : (i : α) → P (Sum.inl i)<VAR>g : (i : β) → P (Sum.inr i)<VAR>x y : α ⊕ β<VAR>h : x = y<GOAL>Sum.rec f g x = cast ⋯ (Sum.rec f g y)
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<VAR>a : α<GOAL>x = Sum.inl a ↔ ∃ h, x.getLeft h = a
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<VAR>b : β<GOAL>x = Sum.inr b ↔ ∃ h, x.getRight h = b
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<VAR>h₁ : x.isLeft = true<VAR>h₂ : x.getLeft?.isSome = true<GOAL>x.getLeft h₁ = x.getLeft?.get h₂
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<VAR>h₁ : x.isRight = true<VAR>h₂ : x.getRight?.isSome = true<GOAL>x.getRight h₁ = x.getRight?.get h₂
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<GOAL>x.getLeft?.isSome = true ↔ x.isLeft = true
<VAR>α : Type u<VAR>β : Type v<VAR>x : α ⊕ β<GOAL>x.getRight?.isSome = true ↔ x.isRight = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq α<VAR>DecidableEq (α ⊕ β)<VAR>f : α → γ<VAR>g : β → γ<VAR>i : α<VAR>x : γ<GOAL>Function.update (Sum.elim f g) (Sum.inl i) x = Sum.elim (Function.update f i x) g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq β<VAR>DecidableEq (α ⊕ β)<VAR>f : α → γ<VAR>g : β → γ<VAR>i : β<VAR>x : γ<GOAL>Function.update (Sum.elim f g) (Sum.inr i) x = Sum.elim f (Function.update g i x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq α<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : α<VAR>x : γ<GOAL>Function.update f (Sum.inl i) x ∘ Sum.inl = Function.update (f ∘ Sum.inl) i x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq α<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i j : α<VAR>x : γ<GOAL>Function.update f (Sum.inl i) x (Sum.inl j) = Function.update (f ∘ Sum.inl) i x j
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : α<VAR>x : γ<GOAL>Function.update f (Sum.inl i) x ∘ Sum.inr = f ∘ Sum.inr
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : α<VAR>j : β<VAR>x : γ<GOAL>Function.update f (Sum.inl i) x (Sum.inr j) = f (Sum.inr j)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : β<VAR>x : γ<GOAL>Function.update f (Sum.inr i) x ∘ Sum.inl = f ∘ Sum.inl
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : α<VAR>j : β<VAR>x : γ<GOAL>Function.update f (Sum.inr j) x (Sum.inl i) = f (Sum.inl i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq β<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i : β<VAR>x : γ<GOAL>Function.update f (Sum.inr i) x ∘ Sum.inr = Function.update (f ∘ Sum.inr) i x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq β<VAR>DecidableEq (α ⊕ β)<VAR>f : α ⊕ β → γ<VAR>i j : β<VAR>x : γ<GOAL>Function.update f (Sum.inr i) x (Sum.inr j) = Function.update (f ∘ Sum.inr) i x j
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.LeftInverse Sum.swap Sum.swap
<VAR>α : Type u<VAR>β : Type v<GOAL>Function.RightInverse Sum.swap Sum.swap
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h : Sum.LiftRel r s x y<GOAL>x.isLeft = true ↔ y.isLeft = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h : Sum.LiftRel r s x y<GOAL>x.isRight = true ↔ y.isRight = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>c : γ<VAR>h : Sum.LiftRel r s x (Sum.inl c)<GOAL>x.isLeft = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>a : α<VAR>h : Sum.LiftRel r s (Sum.inl a) y<GOAL>y.isLeft = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>d : δ<VAR>h : Sum.LiftRel r s x (Sum.inr d)<GOAL>x.isRight = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>y : γ ⊕ δ<VAR>b : β<VAR>h : Sum.LiftRel r s (Sum.inr b) y<GOAL>y.isRight = true
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h₁ : Sum.LiftRel r s x y<VAR>h₂ : x.isLeft = true<GOAL>∃ a c, r a c ∧ x = Sum.inl a ∧ y = Sum.inl c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h₁ : Sum.LiftRel r s x y<VAR>h₂ : y.isLeft = true<GOAL>∃ a c, r a c ∧ x = Sum.inl a ∧ y = Sum.inl c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h₁ : Sum.LiftRel r s x y<VAR>h₂ : x.isRight = true<GOAL>∃ b d, s b d ∧ x = Sum.inr b ∧ y = Sum.inr d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>h₁ : Sum.LiftRel r s x y<VAR>h₂ : y.isRight = true<GOAL>∃ b d, s b d ∧ x = Sum.inr b ∧ y = Sum.inr d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : α → γ<VAR>g : β → γ<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<VAR>hfg : ∀ (a : α) (b : β), f a ≠ g b<GOAL>Function.Injective (Sum.elim f g)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>f : α → β<VAR>g : α' → β'<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<GOAL>Function.Injective (Sum.map f g)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>f : α → β<VAR>g : α' → β'<VAR>hf : Function.Surjective f<VAR>hg : Function.Surjective g<GOAL>Function.Surjective (Sum.map f g)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>f : α → β<VAR>g : α' → β'<VAR>hf : Function.Bijective f<VAR>hg : Function.Bijective g<GOAL>Function.Bijective (Sum.map f g)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Injective (Sum.map f g) ↔ Function.Injective f ∧ Function.Injective g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Surjective (Sum.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>f : α → γ<VAR>g : β → δ<GOAL>Function.Bijective (Sum.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → γ<VAR>g : β → γ<VAR>i : α<VAR>c : γ<GOAL>Sum.elim (Function.update f i c) g = Function.update (Sum.elim f g) (Sum.inl i) c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → γ<VAR>g : β → γ<VAR>i : β<VAR>c : γ<GOAL>Sum.elim f (Function.update g i c) = Function.update (Sum.elim f g) (Sum.inr i) c
<VAR>F : Sort u_1<VAR>α : outParam (Sort u_2)<VAR>β : outParam (α → Sort u_3)<VAR>self : DFunLike F α β<GOAL>Function.Injective DFunLike.coe
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<GOAL>DFunLike.coe = fun f => ⇑f
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<GOAL>Function.Injective fun f => ⇑f
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<GOAL>⇑f = ⇑g ↔ f = g
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<VAR>h : ⇑f = ⇑g<GOAL>f = g
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<GOAL>f = g ↔ ⇑f = ⇑g
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<VAR>h : ∀ (x : α), f x = g x<GOAL>f = g
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<GOAL>f = g ↔ ∀ (x : α), f x = g x
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<VAR>h₁ : f = g<VAR>x : α<GOAL>f x = g x
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<GOAL>f ≠ g ↔ ∃ a, f a ≠ g a
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>f g : F<VAR>h : f ≠ g<GOAL>∃ x, f x ≠ g x
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : α → Sort u_3<VAR>i : DFunLike F α β<VAR>∀ (a : α), Subsingleton (β a)<GOAL>Subsingleton F
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>i : FunLike F α β<VAR>f g : F<VAR>x y : α<VAR>h₁ : f = g<VAR>h₂ : x = y<GOAL>f x = g y
<VAR>F : Sort u_1<VAR>α : Sort u_2<VAR>β : Sort u_3<VAR>i : FunLike F α β<VAR>f : F<VAR>x y : α<VAR>h₂ : x = y<GOAL>f x = f y
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>x : P.last.M<VAR>a₁ : P.A<VAR>f₁ : P.last.B a₁ → P.last.M<VAR>h₁ : x.dest = ⟨a₁, f₁⟩<VAR>a₂ : P.A<VAR>f₂ : P.last.B a₂ → P.last.M<VAR>h₂ : x.dest = ⟨a₂, f₂⟩<VAR>f' : MvPFunctor.M.Path P x ⟹ α<GOAL>MvPFunctor.M.dest' P h₁ f' = MvPFunctor.M.dest' P h₂ f'
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>x : P.last.M<VAR>a : P.A<VAR>f : P.last.B a → P.last.M<VAR>h : x.dest = ⟨a, f⟩<VAR>f' : MvPFunctor.M.Path P x ⟹ α<GOAL>MvPFunctor.M.dest P ⟨x, f'⟩ = MvPFunctor.M.dest' P h f'
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₀ : β → P.A<VAR>g₁ : (b : β) → P.drop.B (g₀ b) ⟹ α<VAR>g₂ : (b : β) → P.last.B (g₀ b) → β<VAR>x : β<GOAL>MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) = ⟨g₀ x, TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ ∘ g₂ x)⟩
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : β → ↑P (α ::: β)<VAR>x : β<GOAL>MvPFunctor.M.dest P (MvPFunctor.M.corec P g x) = (TypeVec.id ::: MvPFunctor.M.corec P g) <$$> g x