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

Goal state before:
pp: J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ (((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ≫ (V F i j).ι) z =
    (V F i j).ι ((pullback.fst (V F i j).ι (V F i k).ι) x)

Tactic:
simpa using

Goal state after:
J : Type w
inst✝² : Category.{v, w} J
F : J ⥤ Scheme
inst✝¹ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝ : (F ⋙ forget).IsLocallyDirected
i j k : J
x : ↥(pullback (V F i j).ι (V F i k).ι)
k₁ : (k : J) × (k ⟶ i) × (k ⟶ j)
k₂ : (k_1 : J) × (k_1 ⟶ i) × (k_1 ⟶ k)
l : J
hli : l ⟶ k₁.fst
hlk : l ⟶ k₂.fst
z : (F ⋙ forget).obj l
hy₁ : (F.map k₁.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hli)) z) = ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
hy₂ : (F.map k₂.snd.1) ((ConcreteCategory.hom ((F ⋙ forget).map hlk)) z) = ↑((pullback.snd (V F i j).ι (V F i k).ι) x)
α : F.obj l ⟶ pullback (V F i j).ι (V F i k).ι :=
  pullback.lift ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯)
    ((Hom.isoOpensRange (F.map (hli ≫ k₁.snd.1))).hom ≫ (F.obj i).homOfLE ⋯) ⋯
this : IsOpenImmersion α
⊢ (TopCat.Hom.hom (F.map k₁.snd.1).base) ((TopCat.Hom.hom (F.map hli).base) z) =
    ↑((pullback.fst (V F i j).ι (V F i k).ι) x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨iy, y⟩
⊢ (α ix) x = (α iy) y

Tactic:
simpa using

Goal state after:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
ix : ι
x : ↥(f ix)
iy : ι
y : ↥(f iy)
e : (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨ix, x⟩ = (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨iy, y⟩
⊢ (α ix) x = (α iy) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
i : ι
⊢ IsOpenMap fun a ↦ (⇑(Sigma.desc α) ∘ ⇑(sigmaMk f)) ⟨i, a⟩

Tactic:
simpa using

Goal state after:
case left.refine_3
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
i : ι
⊢ IsOpenMap fun a ↦ (α i) a
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) ≫
      F.map k₁.snd.1 =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) ≫
      F.map k₂.snd.1

Tactic:
simpa using

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
⊢ pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.opensRange (F.map k₁.snd.1)).ι =
    pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.opensRange (F.map k₂.snd.1)).ι
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
i j : σ
hij : i ≠ j
⊢ (Disjoint on fun x ↦ Set.range ⇑(f x)) i j

Tactic:
simpa using

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
i j : σ
hij : i ≠ j
⊢ Set.range ⇑(f i) ∩ Set.range ⇑(f j) = ∅
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a
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₀
⊢ pullback.snd 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

Tactic:
rw [← Iso.inv_comp_eq, pullbackSymmetry_inv_comp_snd, pullback.lift_fst, Category.comp_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ ?m.101

Tactic:
simpa using

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this✝ : IsOpenImmersion (Sigma.desc f)
x : ↥S
hx : x ∈ ⊤
this : x ∈ ⨆ i, Scheme.Hom.opensRange (f i)
⊢ ?m.101
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
X' : C
f' :
  ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj
      (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ⟶
    X'
⊢ D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ≫ f' =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          (unop (op ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 (unop (op U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ f'

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j k : D.J
U : Opens ↑↑(D.U i)
X' : C
f' :
  ((TopCat.Presheaf.pushforward C (D.f j k).base).obj (D.V (j, k)).presheaf).obj
      (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ⟶
    X'
⊢ D.opensImagePreimageMap i j U ≫ (D.f j k).c.app (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) ≫ f' =
    (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
      invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ f'
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2

Tactic:
have : IsOpenImmersion α := by
    have : IsOpenImmersion (α ≫ pullback.fst _ _) := by
      simp only [pullback.lift_fst, α]; infer_instance
    exact .of_comp _ (pullback.fst _ _)

Goal state after:
J : Type w
inst✝³ : Category.{v, w} J
F : J ⥤ Scheme
inst✝² : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝¹ : (F ⋙ forget).IsLocallyDirected
inst✝ : Quiver.IsThin J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd.1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd.1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst
hlj : l ⟶ k₂.fst
y : (F ⋙ forget).obj l
hy₁ :
  (ConcreteCategory.hom ((F ⋙ forget).map hli)) y =
    (pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).inv) x
hy₂ :
  (ConcreteCategory.hom ((F ⋙ forget).map hlj)) y =
    (pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).inv) x
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ (Hom.isoOpensRange (F.map k₁.snd.1)).hom)
    (F.map hlj ≫ (Hom.isoOpensRange (F.map k₂.snd.1)).hom) ⋯
this : IsOpenImmersion α
⊢ ∃ U_1,
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₁.snd.1)).inv ≫ F.map k₁.snd.2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            (Hom.isoOpensRange (F.map k₂.snd.1)).inv ≫ F.map k₂.snd.2
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
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p1 𝒰 f g =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.fst

Tactic:
simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p1 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.fst
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case convert_2
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
⊢ ⨆ i, Scheme.Hom.opensRange (fi i) = ⊤

Tactic:
simpa using

Goal state after:
case convert_2
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
⊢ Codisjoint (Scheme.Hom.opensRange (fi WalkingPair.left)) (Scheme.Hom.opensRange (fi WalkingPair.right))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: 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
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.left WalkingPair.right

Tactic:
simpa using

Goal state after:
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
i j : WalkingPair
hij : WalkingPair.left ≠ WalkingPair.right
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (WalkingPair.rec f g x)) WalkingPair.left WalkingPair.right
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: 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
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (fi x)) WalkingPair.right WalkingPair.left

Tactic:
simpa using

Goal state after:
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
i j : WalkingPair
hij : WalkingPair.right ≠ WalkingPair.left
⊢ Function.onFun Disjoint (fun x ↦ Scheme.Hom.opensRange (WalkingPair.rec f g x)) WalkingPair.right WalkingPair.left
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
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ gluedLift 𝒰 f g s ≫ p2 𝒰 f g =
    Multicoequalizer.π (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).diagram b ≫
      Cover.fromGlued (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰) ≫ s.snd

Tactic:
simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s : PullbackCone f g
b : (MultispanShape.prod (Cover.gluedCover (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)).J).R
⊢ ((Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫
        Cover.glueMorphisms (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰)
          (fun i ↦
            ((pullbackSymmetry s.fst (𝒰.f i)).hom ≫ pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯) ≫
              (gluing 𝒰 f g).ι i)
          ⋯) ≫
      p2 𝒰 f g =
    (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f b ≫ s.snd
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} → (f : Z ⟶ X ⨿ Y) → IsColimit (BinaryCofan.mk (pullback.fst f coprod.inl) (pullback.fst f coprod.inr))

Tactic:
refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some

Goal state after:
case refine_2
ι : Type u
f✝ : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
Z : Scheme
f : Z ⟶ X ⨿ Y
⊢ IsCompl (Scheme.Hom.opensRange (pullback.fst f coprod.inl)) (Scheme.Hom.opensRange (pullback.fst f coprod.inr))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X✝ Y✝ : Scheme
X Y : Scheme
c : BinaryCofan X Y
hc : IsColimit c
⊢ {Z : Scheme} →
    (f : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt) →
      IsColimit
        (BinaryCofan.mk
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inl)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inl) ⋯).fst
          (PullbackCone.mk (pullback.fst f (BinaryCofan.mk coprod.inl coprod.inr).inr)
              (pullback.snd f (BinaryCofan.mk coprod.inl coprod.inr).inr) ⋯).fst)

Tactic:
· dsimp
      refine fun {Z} f ↦ (nonempty_isColimit_binaryCofanMk_of_isCompl _ _ ?_).some
      rw [Scheme.Hom.opensRange_pullbackFst, Scheme.Hom.opensRange_pullbackFst]
      convert! (isCompl_range_inl_inr X Y).map (CompleteLatticeHom.setPreimage f)
      simp [isCompl_iff, disjoint_iff, codisjoint_iff, ← TopologicalSpace.Opens.coe_inj]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case hom_inv_id.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 : 𝒰.I₀
⊢ (pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
        pullback.lift ((gluing 𝒰 f g).ι i) (pullback.fst (𝒰.f i ≫ f) g) ⋯) ≫
      pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    𝟙 (pullback (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i)

Tactic:
simpa using

Goal state after:
case hom_inv_id.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 : 𝒰.I₀
⊢ pullback.lift (pullback.snd (p1 𝒰 f g) (𝒰.f i)) (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ⋯ ≫
      Multicoequalizer.π (gluing 𝒰 f g).diagram i =
    pullback.fst (p1 𝒰 f g) (𝒰.f i)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    ((pullback.fst (D.f j k) (D.f j i)).c.app
          (op
            ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
              ((Opens.map (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j).base).1 U))) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
              (pullback (D.f j k) (D.f j i)).presheaf).map
          (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f j k) (D.f j i))
              ((Opens.map (D.t' j k i).base).1
                ((Opens.map (pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k).base).1 U)) ≫
            (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
              ((TopCat.Presheaf.pushforward C (D.t j k).base).obj (D.V (j, k)).presheaf).map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
simp_rw [Category.assoc, Functor.op_obj, comp_base, Opens.map_comp_obj,
              TopCat.Presheaf.pushforward_obj_map]

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
              ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        (pullback (D.f j k) (D.f j i)).presheaf.map
            ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op ≫
          (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
            invApp (pullback.fst (D.f j k) (D.f j i))
                ((Opens.map (D.t' j k i).base).1
                  ((Opens.map (pullback.fst (D.f k i) (D.f k j)).base).obj
                    ((Opens.map (D.t k i).base).obj ((Opens.map (D.f i k).base).obj U)))) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
simpa using

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
⊢ Set.range ⇑f ⊆ ⋃ i, ↑(U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ Set.range ⇑f ⊆ Set.range ⇑(⨆ i, U i).ι

Tactic:
simpa using

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ Set.range ⇑f ⊆ ⋃ i, ↑(U i)