mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)

pp: case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.snd (𝒰.f y) (𝒰.f x)

Tactic:
<;>

Goal state after:
case h₀
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.fst (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.fst (𝒰.f y) (𝒰.f x)

case h₁
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ (gluedCoverT' 𝒰 x y z ≫ pullback.snd (pullback.fst (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))) ≫
      pullback.snd (𝒰.f y) (𝒰.f x) =
    (pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫
        (pullbackSymmetry (𝒰.f x) (𝒰.f y)).hom) ≫
      pullback.snd (𝒰.f y) (𝒰.f x)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
y : ↥(gluedCover 𝒰).glued
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
h : (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) = (fromGlued 𝒰) y
⊢ ((gluedCover 𝒰).ι i) x = y

Tactic:
obtain ⟨j, y, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective y

Goal state after:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) = (fromGlued 𝒰) (((gluedCover 𝒰).ι j) y)
⊢ ((gluedCover 𝒰).ι i) x = ((gluedCover 𝒰).ι j) y
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

Tactic:
<;>

Goal state after:
case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
⊢ t 𝒰 f g i i ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i) =
    𝟙 (v 𝒰 f g i i) ≫ pullback.snd (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)

Tactic:
<;>

Goal state after:
case h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    𝟙 (pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k)) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hf.e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g =
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          (pullbackSymmetry s.fst (𝒰.f j)).hom) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f j ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g =
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          (pullbackSymmetry s.fst (𝒰.f j)).hom) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ≫
      pullback.snd (𝒰.f j ≫ f) g

Tactic:
<;>

Goal state after:
case hf.e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.fst (𝒰.f j ≫ f) g =
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          (pullbackSymmetry s.fst (𝒰.f j)).hom) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ≫
      pullback.fst (𝒰.f j ≫ f) g

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
i j : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ ((gluedLiftPullbackMap 𝒰 f g s i j ≫ t 𝒰 f g i j) ≫ pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i)) ≫
      pullback.snd (𝒰.f j ≫ f) g =
    ((pullback.snd ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
            ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ≫
          (pullbackSymmetry s.fst (𝒰.f j)).hom) ≫
        pullback.map (𝒰.f j) s.fst (𝒰.f j ≫ f) g (𝟙 (𝒰.X j)) s.snd f ⋯ ⋯) ≫
      pullback.snd (𝒰.f j ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.left ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.left

pp: case right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.right ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.right

Tactic:
<;>

Goal state after:
case left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.left ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.left

case right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
⊢ Cofan.inj (BinaryCofan.mk f g) WalkingPair.right ≫ (Iso.refl (BinaryCofan.mk f g).pt).hom = c'.inj WalkingPair.right
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.left)

pp: case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.right)

Tactic:
<;>

Goal state after:
case convert_1.left
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.left)

case convert_1.right
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
hf : IsCompl (Scheme.Hom.opensRange f) (Scheme.Hom.opensRange g)
c' : Cofan fun j ↦ WalkingPair.casesOn j X Y := Cofan.mk S fun j ↦ WalkingPair.casesOn j f g
i : BinaryCofan.mk f g ≅ c' := Cofan.ext (Iso.refl (BinaryCofan.mk f g).pt) ⋯
fi : (j : WalkingPair) → WalkingPair.casesOn j X Y ⟶ S := fun j ↦ WalkingPair.casesOn j f g
⊢ IsOpenImmersion (fi WalkingPair.right)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl

pp: case refine_1.refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr

Tactic:
<;>

Goal state after:
case refine_1.refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl = Scheme.Hom.opensRange coprod.inl

case refine_1.refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
⊢ f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr = Scheme.Hom.opensRange coprod.inr
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_1.refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inl)

pp: case refine_1.refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inr)

Tactic:
<;>

Goal state after:
case refine_1.refine_1
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inl) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inl)

case refine_1.refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
X' Y' : Scheme
αX : X' ⟶ X
αY : Y' ⟶ Y
f : (BinaryCofan.mk coprod.inl coprod.inr).pt ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt
h₁ : αX ≫ coprod.inl = coprod.inl ≫ f
h₂ : αY ≫ coprod.inr = coprod.inr ≫ f
h₁' :
  ∀ (x : ↥X'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inl.base) x) =
      (TopCat.Hom.hom coprod.inl.base) ((TopCat.Hom.hom αX.base) x)
h₂' :
  ∀ (x : ↥Y'),
    (TopCat.Hom.hom f.base) ((TopCat.Hom.hom coprod.inr.base) x) =
      (TopCat.Hom.hom coprod.inr.base) ((TopCat.Hom.hom αY.base) x)
x : ↥(X' ⨿ Y')
⊢ x ∈ ↑(f ⁻¹ᵁ Scheme.Hom.opensRange coprod.inr) ↔ x ∈ ↑(Scheme.Hom.opensRange coprod.inr)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g

pp: case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
<;>

Goal state after:
case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.fst (𝒰.f i ≫ f) g =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.fst (𝒰.f i ≫ f) g

case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullback.fst (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫
        pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g =
    ((pullbackFstιToV 𝒰 f g i j ≫ t 𝒰 f g j i) ≫ pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j)) ≫
      pullback.snd (𝒰.f i ≫ f) g
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x))).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x))).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal

Tactic:
<;>

Goal state after:
case inl
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of R))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inl x))).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x)).asIdeal

case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
⊢ ((coprodSpec R S) ((coprodMk (Spec (CommRingCat.of R)) (Spec (CommRingCat.of S))) (Sum.inr x))).asIdeal =
    ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i : 𝒰.I₀
j : (Precoverage.ZeroHypercover.pullback₁ (pullback.fst (p1 𝒰 f g) (𝒰.f i)) (gluing 𝒰 f g).openCover).I₀
⊢ (pullbackFstιToV 𝒰 f g i j ≫ fV 𝒰 f g j i) ≫ (gluing 𝒰 f g).ι j =
    pullback.snd (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ((gluing 𝒰 f g).openCover.f j) ≫ (gluing 𝒰 f g).openCover.f j

Tactic:
simp_rw [pullbackFstιToV_fst, GlueData.openCover_f]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ IsIso (coprodComparison Scheme.Spec (op R) (op S))

Tactic:
have : coprodComparison Scheme.Spec (.op R) (.op S) ≫ (Spec.map
    ((limit.isoLimitCone ⟨_, CommRingCat.prodFanIsLimit R S⟩).inv ≫
      (opProdIsoCoprod R S).unop.inv)) = coprodSpec R S := by
    ext1
    · rw [coprodComparison_inl_assoc, coprodSpec, coprod.inl_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inl,
        limit.isoLimitCone_inv_π]
      rfl
    · rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]
      rfl

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
this :
  coprodComparison Scheme.Spec (op R) (op S) ≫
      Spec.map
        ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
          (opProdIsoCoprod R S).unop.inv) =
    coprodSpec ↑R ↑S
⊢ IsIso (coprodComparison Scheme.Spec (op R) (op S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case pos
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

pp: case neg
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : ¬j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

Tactic:
<;>

Goal state after:
case pos
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j

case neg
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
i : ι
R : ι → Type (max u_1 u)
inst✝ : (i : ι) → CommRing (R i)
this : Algebra ((i : ι) → R i) (R i) := (Pi.evalRingHom R i).toAlgebra
j : ι
h : ¬j = i
⊢ (Function.update 0 i 1 * Function.update 0 i 1) j = Function.update 0 i 1 j