ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i ≫ AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j = 𝟙 (CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).U i = CategoryTheory.Limits.pullback (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<GOAL>∀ (x : 𝒰.J × 𝒰.J), (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V x = match x with | (i, j) => AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).J = 𝒰.J
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).t i j = AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).f i j = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).t' i j k = AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>j : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j = CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram j
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<GOAL>AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g ≫ f = AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g ≫ g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>s : CategoryTheory.Limits.PullbackCone f g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) = CategoryTheory.Limits.pullback.fst ((𝒰.pullbackCover s.fst).map i) ((𝒰.pullbackCover s.fst).map j) ≫ (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom ≫ CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (𝒰.map i ≫ f) g (𝟙 (𝒰.obj i)) s.snd f ⋯ ⋯
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>s : CategoryTheory.Limits.PullbackCone f g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map j) = CategoryTheory.Limits.pullback.snd ((𝒰.pullbackCover s.fst).map i) ((𝒰.pullbackCover s.fst).map j) ≫ CategoryTheory.Limits.pullback.snd s.fst (𝒰.map j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s ≫ AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g = s.fst
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>s : CategoryTheory.Limits.PullbackCone f g<GOAL>AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s ≫ AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g = s.snd
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j ≫ CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)) ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i j : 𝒰.J<GOAL>AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV 𝒰 f g i j ≫ CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.map j ≫ f) g ≫ 𝒰.map j) (𝒰.map i) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)) ((AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι j) ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)) (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i) ≫ AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) ⋯ ≫ (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom ≫ CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom ≫ CategoryTheory.Limits.pullback.snd (𝒰.map i ≫ f) g = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i) ≫ AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i) = (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i) = CategoryTheory.Limits.pullback.fst (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom ≫ CategoryTheory.Limits.Multicoequalizer.π (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).diagram i = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (𝒰.map i)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (𝒰.map i ≫ f) g<GOAL>CategoryTheory.Limits.HasPullback f g
<VAR>B C : CommRingCat<VAR>X : AlgebraicGeometry.Scheme<VAR>f : X ⟶ AlgebraicGeometry.Spec C<VAR>g : AlgebraicGeometry.Spec B ⟶ AlgebraicGeometry.Spec C<GOAL>CategoryTheory.Limits.HasPullback f g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).J = 𝒰.J
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).obj i = CategoryTheory.Limits.pullback (𝒰.map i ≫ f) g
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (𝒰.map i ≫ f) g f g (𝒰.map i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).map i = CategoryTheory.Limits.pullback.map f (𝒰.map i ≫ g) f g (𝟙 X) (𝒰.map i) (𝟙 Z) ⋯ ⋯
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).obj i = CategoryTheory.Limits.pullback f (𝒰.map i ≫ g)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfRight 𝒰 f g).J = 𝒰.J
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>ij : 𝒰X.J × 𝒰Y.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).obj ij = CategoryTheory.Limits.pullback (𝒰X.map ij.1 ≫ f) (𝒰Y.map ij.2 ≫ g)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).J = (𝒰X.J × 𝒰Y.J)
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰X : X.OpenCover<VAR>𝒰Y : Y.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>ij : 𝒰X.J × 𝒰Y.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight 𝒰X 𝒰Y f g).map ij = CategoryTheory.Limits.pullback.map (𝒰X.map ij.1 ≫ f) (𝒰Y.map ij.2 ≫ g) f g (𝒰X.map ij.1) (𝒰Y.map ij.2) (𝟙 Z) ⋯ ⋯
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).obj i = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i))
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).J = 𝒰.J
<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>𝒰 : Z.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>i : 𝒰.J<GOAL>(AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.map i)) (CategoryTheory.Limits.pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯
<VAR>R S T : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<GOAL>(AlgebraicGeometry.pullbackSpecIso R S T).inv ≫ CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
<VAR>R S T : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<GOAL>(AlgebraicGeometry.pullbackSpecIso R S T).inv ≫ CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)
<VAR>R S T : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<GOAL>(AlgebraicGeometry.pullbackSpecIso R S T).hom ≫ AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))
<VAR>R S T : Type u<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<GOAL>(AlgebraicGeometry.pullbackSpecIso R S T).hom ≫ AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T)))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>Levenshtein.defaultCost.substitute a b = if a = b then 0 else 1
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>∀ (x : α), Levenshtein.defaultCost.delete x = 1
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>∀ (x : α), Levenshtein.defaultCost.insert x = 1
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a : α<GOAL>(Levenshtein.weightCost f).delete a = f a
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>a b : α<GOAL>(Levenshtein.weightCost f).substitute a b = max (f a) (f b)
<VAR>α : Type u_1<VAR>f : α → ℕ<VAR>b : α<GOAL>(Levenshtein.weightCost f).insert b = f b
<VAR>b : String<GOAL>Levenshtein.stringLengthCost.insert b = b.length
<VAR>a : String<GOAL>Levenshtein.stringLengthCost.delete a = a.length
<VAR>a b : String<GOAL>Levenshtein.stringLengthCost.substitute a b = max a.length b.length
<VAR>b : String<GOAL>Levenshtein.stringLogLengthCost.insert b = (b.length + 1).log2
<VAR>a b : String<GOAL>Levenshtein.stringLogLengthCost.substitute a b = max (a.length + 1).log2 (b.length + 1).log2
<VAR>a : String<GOAL>Levenshtein.stringLogLengthCost.delete a = (a.length + 1).log2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>d : δ<VAR>ds : List δ<VAR>w : 0 < (d :: ds).length<VAR>w' : 0 < ds.length<GOAL>Levenshtein.impl C (x :: xs) y ⟨d :: ds, w⟩ = match Levenshtein.impl C xs y ⟨ds, w'⟩ with | ⟨r, w⟩ => ⟨min (C.delete x + r[0]) (min (C.insert y + d) (C.substitute x y + ds[0])) :: r, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>d : δ<VAR>ds : List δ<VAR>w : 0 < (d :: ds).length<VAR>h : 0 < (Levenshtein.impl C (x :: xs) y ⟨d :: ds, w⟩).val.length<VAR>w' : 0 < ds.length<GOAL>(Levenshtein.impl C (x :: xs) y ⟨d :: ds, w⟩).val[0] = match Levenshtein.impl C xs y ⟨ds, w'⟩ with | ⟨r, w⟩ => min (C.delete x + r[0]) (min (C.insert y + d) (C.substitute x y + ds[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>y : β<VAR>d : { r // 0 < r.length }<VAR>w : d.val.length = xs.length + 1<GOAL>(Levenshtein.impl C xs y d).val.length = xs.length + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C xs ys).val.length = xs.length + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>Levenshtein.impl C xs y (suffixLevenshtein C xs ys) = suffixLevenshtein C xs (y :: ys)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<GOAL>(suffixLevenshtein C [] []).val = [0]
<VAR>α : Type u_1<VAR>x : List α<VAR>w : x.length = 1<GOAL>let_fun this := ⋯;
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>ys : List β<GOAL>(suffixLevenshtein C [] ys).val = [levenshtein C [] ys]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>suffixLevenshtein C xs (y :: ys) = Levenshtein.impl C xs y (suffixLevenshtein C xs ys)
<VAR>δ : Type u_3<VAR>x y : { r // 0 < r.length }<VAR>w₀ : x.val[0] = y.val[0]<VAR>w : x.val.tail = y.val.tail<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>ys : List β<GOAL>suffixLevenshtein C (x :: xs) ys = ⟨levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C (x :: xs) ys).val = levenshtein C (x :: xs) ys :: (suffixLevenshtein C xs ys).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<VAR>w : 0 < (suffixLevenshtein C (x :: xs) (y :: ys)).val.length<GOAL>(suffixLevenshtein C (x :: xs) (y :: ys)).val[0] = match suffixLevenshtein C xs (y :: ys) with | ⟨dx, property⟩ => match suffixLevenshtein C (x :: xs) ys with | ⟨dy, property_1⟩ => match suffixLevenshtein C xs ys with | ⟨dxy, property_2⟩ => min (C.delete x + dx[0]) (min (C.insert y + dy[0]) (C.substitute x y + dxy[0]))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>ys : List β<GOAL>(suffixLevenshtein C xs ys).val = List.map (fun xs' => levenshtein C xs' ys) xs.tails
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<GOAL>levenshtein C [] [] = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>y : β<VAR>ys : List β<GOAL>levenshtein C [] (y :: ys) = C.insert y + levenshtein C [] ys
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<GOAL>levenshtein C (x :: xs) [] = C.delete x + levenshtein C xs []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>AddZeroClass δ<VAR>Min δ<VAR>C : Levenshtein.Cost α β δ<VAR>x : α<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>levenshtein C (x :: xs) (y :: ys) = min (C.delete x + levenshtein C xs (y :: ys)) (min (C.insert y + levenshtein C (x :: xs) ys) (C.substitute x y + levenshtein C xs ys))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>(↑(suffixLevenshtein C xs ys)).minimum ≤ ↑(levenshtein C xs (y :: ys))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>(↑(suffixLevenshtein C xs ys)).minimum ≤ (↑(suffixLevenshtein C xs (y :: ys))).minimum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>(↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs (ys₁ ++ ys₂))).minimum
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>(↑(suffixLevenshtein C xs ys₂)).minimum ≤ ↑(levenshtein C xs (ys₁ ++ ys₂))