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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ Set.range (⇑(TopCat.Hom.hom f.base) ∘ ⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base)) = Set.range ⇑U.ι

Tactic:
Set.range_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ ⇑(TopCat.Hom.hom f.base) '' Set.range ⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base) = Set.range ⇑U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.range (⇑V.ι ∘ ⇑(V.ι ⁻¹ᵁ U).ι) = ↑U

Tactic:
Set.range_comp,

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ ⇑V.ι '' Set.range ⇑(V.ι ⁻¹ᵁ U).ι = ↑U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f : ↑R
⊢ Set.range ⇑(Scheme.Opens.ι (PrimeSpectrum.basicOpen f)) =
    Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))

Tactic:
simp only [Scheme.Opens.range_ι]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f : ↑R
⊢ ↑(PrimeSpectrum.basicOpen f) = Set.range ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f))))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ pullback f U.ι ≅ ↑(f ⁻¹ᵁ U)

Tactic:
refine IsOpenImmersion.isoOfRangeEq (pullback.fst f _) (Scheme.Opens.ι _) ?_

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ Set.range ⇑(pullback.fst f U.ι) = Set.range ⇑(f ⁻¹ᵁ U).ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ pullback f U.ι ≅ ↑(f ⁻¹ᵁ U)

Tactic:
refine IsOpenImmersion.isoOfRangeEq (pullback.fst f _) (Scheme.Opens.ι _) ?_
  simp [IsOpenImmersion.range_pullbackFst]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.map (eqToHom ⋯).op ≫ (↑U).presheaf.germ ⊤ x True.intro))
      (closedPoint ↑((↑U).presheaf.stalk x)) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
(Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial),

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.germ (U.ι ''ᵁ ⊤) ↑x ⋯ ≫ (U.stalkIso x).inv))
      (closedPoint ↑((↑U).presheaf.stalk x)) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range
      (⇑(TopCat.Hom.hom U.ι.base) ∘
        ⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)) =
    ↑U

Tactic:
Set.range_comp,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ ⇑(TopCat.Hom.hom U.ι.base) ''
      Set.range
        (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base)) =
    ↑U
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom ((structurePresheafInCommRingCat R).germ U x hxU))
        ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r)) •
      (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU)) m

Tactic:
refine .trans ?_ (PresheafOfModules.germ_smul ..)

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
r : R
m : (structureSheafInType R M).obj.obj (op U)
⊢ (↑(AddCommGrpCat.Hom.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))).toFun (r • m) =
    (ConcreteCategory.hom (Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU))
      ((algebraMap R ((structureSheafInType R R).obj.obj (op U))) ((RingHom.id R) r) • m)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  IsUnit
    ((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
        (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
      ((ConcreteCategory.hom (toStalk R x)) f))
⊢ IsUnit ((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)

Tactic:
rw [Module.End.isUnit_iff] at this ⊢

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↑(PrimeSpectrum.Top R)
f : R
hf : x ∈ basicOpen f
this :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↑((structurePresheafInModuleCat R M).stalk x))) f)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
⊢ toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
by
  unfold toSpecΓ
  have := X.toΓSpecSheafedSpace_app_spec 1
  unfold toToΓSpecMapBasicOpen toΓSpecMapBasicOpen at this
  rw! [basicOpen_one] at this
  convert! this
  exact (X.presheaf.map_id ..).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
m : M
⊢ (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) (r • m)) =
    (RingHom.id R) r • (ConcreteCategory.hom (germ (moduleStructurePresheaf R M).presheaf ⊤ x ⋯)) ((toOpenₗ R M ⊤) m)

Tactic:
by
    change _ = toStalk R x r • TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf _ _ _ _
    rw [map_smul]
    refine .trans ?_ ((moduleStructurePresheaf R M).germ_smul ..)
    congr 1
    exact (IsScalarTower.algebraMap_smul Γ(R, _) (M := Γ(M, _)) _ _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case e_a
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
r : R
α : stalk (moduleStructurePresheaf R R).presheaf x ≅
  (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj ((structurePresheafInCommRingCat R).stalk x) :=
  Limits.colimit.isoColimitCocone
    {
      cocone :=
        (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
          (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
      isColimit :=
        Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
          (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ToType ((moduleStructurePresheaf R R).presheaf.obj (op U))
this :
  germ (moduleStructurePresheaf R R).presheaf U x hxU ≫ α.hom =
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map ((structurePresheafInCommRingCat R).germ U x hxU)
⊢ (CommRingCat.Hom.hom ((structurePresheafInCommRingCat R).germ U x hxU)) s =
    (Limits.colimit.isoColimitCocone
            {
              cocone :=
                (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).mapCocone
                  (Limits.colimit.cocone ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)),
              isColimit :=
                Limits.isColimitOfPreserves (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
                  (Limits.colimit.isColimit
                    ((OpenNhds.inclusion x).op ⋙ structurePresheafInCommRingCat R)) }).addCommGroupIsoToAddEquiv.toFun
      ((ConcreteCategory.hom (germ (moduleStructurePresheaf R R).presheaf U x hxU)) s)

Tactic:
exact congr($this _).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : IsUnit ((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ IsUnit ((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)

Tactic:
rw [Module.End.isUnit_iff] at this ⊢

Goal state after:
R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
y : ↑(PrimeSpectrum.Top S)
this✝² : Module R N := Module.compHom N σ
this✝¹ : Algebra R S := σ.toAlgebra
this✝ : IsScalarTower R S N
f' : M →ₗ[R] N :=
  let __spread.0 := f;
  { toAddHom := __spread.0.toAddHom, map_smul' := ⋯ }
x : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl
this : Function.Bijective ⇑((algebraMap S (Module.End S (LocalizedModule y.asIdeal.primeCompl N))) ↑⟨σ ↑x, ⋯⟩)
⊢ Function.Bijective ⇑((algebraMap R (Module.End R (LocalizedModule y.asIdeal.primeCompl N))) ↑x)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
I J : Ideal ↑Γ(X, U)
⊢ I = J ↔
    ∀ (x : ↥X) (h : x ∈ U),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I =
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) J

Tactic:
by
  simp_rw [le_antisymm_iff, hU.ideal_le_iff, forall_and]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ (⋂ i, PrimeSpectrum.zeroLocus {↑i})ᶜ = Set.univ ↔ Ideal.span s = ⊤

Tactic:
Set.compl_univ_iff,

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋂ i, PrimeSpectrum.zeroLocus {↑i} = ∅ ↔ Ideal.span s = ⊤
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ ↑x.asIdeal

Tactic:
not_not

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ ↑x.asIdeal
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case pos
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↥X
hxU : x ∈ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

pp: case neg
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↥X
hxU : x ∉ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
· simpa [hxU] using congr(⟨x, hxU⟩ ∈ $this)

Goal state after:
case neg
X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
this : U.carrier ↓∩ X.zeroLocus ↑(I ⊓ J) = U.carrier ↓∩ (X.zeroLocus ↑I ∪ X.zeroLocus ↑J)
x : ↥X
hxU : x ∉ U
⊢ x ∈ X.zeroLocus ↑(I ⊓ J) ↔ x ∈ X.zeroLocus ↑I ∪ X.zeroLocus ↑J
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
apply pullback.hom_ext <;> simp [pullback.condition]

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w.refine_1
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.LeftInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

pp: case w.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.RightInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)

Tactic:
· intro x
      rw [← ConcreteCategory.comp_apply, ← comp_base, IsIso.inv_hom_id, id_base,
        ConcreteCategory.id_apply]

Goal state after:
case w.refine_2
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(pullback (D.f i j) (D.f i k))
this :
  ⇑(TopCat.Hom.hom (pullback.snd (D.f i j) (D.f i k)).base) =
    ⇑(TopCat.Hom.hom (D.t k i).base) ∘
      ⇑(TopCat.Hom.hom (pullback.fst (D.f k i) (D.f k j)).base) ∘ ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
⊢ Function.RightInverse ⇑(ConcreteCategory.hom (D.t' k i j).base) ⇑(TopCat.Hom.hom (inv (D.t' k i j)).base)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h.right
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt := ⋯
⊢ ((gluedCover 𝒰).t ⟨i, x⟩.fst ⟨j, y⟩.fst ≫ (gluedCover 𝒰).f ⟨j, y⟩.fst ⟨i, x⟩.fst)
      ((ConcreteCategory.hom e.hom) ⟨(x, y), h⟩) =
    ⟨j, y⟩.snd

Tactic:
erw [← ConcreteCategory.comp_apply e.hom, pullbackSymmetry_hom_comp_fst,
      IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right]
    rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ f₁ = f₂

Tactic:
rw [← cancel_epi 𝒰.ulift.fromGlued]

Goal state after:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f₁ f₂ : X ⟶ Y
h : ∀ (x : 𝒰.I₀), 𝒰.f x ≫ f₁ = 𝒰.f x ≫ f₂
⊢ (ulift 𝒰).fromGlued ≫ f₁ = (ulift 𝒰).fromGlued ≫ f₂
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h.inl
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inl x)))
        y =
      (coprodMk X Y) (Sum.inl x)

pp: case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)

Tactic:
· simp only [Sum.elim_inl, coprodMk_inl, exists_apply_eq_apply]

Goal state after:
case h.inr
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥Y
⊢ ∃ y,
    (Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr)
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) (Sum.inr x)))
        y =
      (coprodMk X Y) (Sum.inr x)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case 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
⊢ αX ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f →
    αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
      IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
        IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).inr

Tactic:
h₁

Goal state after:
case 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 ≫ (BinaryCofan.mk coprod.inl coprod.inr).inl = (BinaryCofan.mk coprod.inl coprod.inr).inl ≫ f
⊢ αY ≫ (BinaryCofan.mk coprod.inl coprod.inr).inr = (BinaryCofan.mk coprod.inl coprod.inr).inr ≫ f →
    IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inl αX f (BinaryCofan.mk coprod.inl coprod.inr).inl ∧
      IsPullback (BinaryCofan.mk coprod.inl coprod.inr).inr αY f (BinaryCofan.mk coprod.inl coprod.inr).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:
· simp_rw [t_fst_fst, pullback.lift_fst, pullbackFstιToV_snd, GlueData.openCover_f]

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₀
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.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✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
⊢ m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst →
    m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = gluedLift 𝒰 f g s

Tactic:
h₁

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
s✝ s : PullbackCone f g
m : s.pt ⟶ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).pt
h₁ : m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst
⊢ m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd → m = gluedLift 𝒰 f g s
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
⊢ IsLimit (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯)

Tactic:
by
  apply PullbackCone.isLimitAux'
  intro s
  refine ⟨gluedLift 𝒰 f g s, gluedLift_p1 𝒰 f g s, gluedLift_p2 𝒰 f g s, ?_⟩
  intro m h₁ h₂
  simp_rw [PullbackCone.mk_pt, PullbackCone.mk_π_app] at h₁ h₂
  apply Cover.hom_ext <| 𝒰.pullback₁ s.fst
  intro i
  rw [gluedLift, (Cover.ι_glueMorphisms <| 𝒰.pullback₁ s.fst)]
  dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, PullbackCone.mk_pt, PreZeroHypercover.pullback₁_f, gluing_ι]
  rw [← cancel_epi
    (pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m ≪≫ pullback.congrHom h₁ rfl).hom,
    Iso.trans_hom, Category.assoc, pullback.congrHom_hom, pullback.lift_fst_assoc,
    Category.comp_id, pullbackRightPullbackFstIso_hom_fst_assoc, pullback.condition]
  conv_lhs => rhs; rw [← pullbackP1Iso_hom_ι]
  simp_rw [← Category.assoc]
  congr 1
  apply pullback.hom_ext
  · simp_rw [Category.assoc, pullbackP1Iso_hom_fst, pullback.lift_fst, Category.comp_id,
      pullbackSymmetry_hom_comp_fst, pullback.lift_snd, Category.comp_id,
      pullbackRightPullbackFstIso_hom_snd]
  · simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd,
      pullbackSymmetry_hom_comp_snd_assoc, pullback.lift_fst_assoc, Category.comp_id,
      pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc, h₂]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtSource P
inst✝ : P.IsMultiplicative
hP : ∀ {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover Y
h : ∀ (i : 𝒰.I₀), P (pullback.snd f (𝒰.f i))
⊢ P f

Tactic:
· rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
    intro i
    rw [← Scheme.Cover.pullbackHom_map]
    exact P.comp_mem _ _ (h i) (of_isOpenImmersion _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case hpostcomp
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
H : targetAffineLocally P f
U : Z.Opens
hU : IsAffineOpen U
this : IsAffine ↑(e.hom ⁻¹ᵁ U)
⊢ P (f ∣_ e.hom ⁻¹ᵁ U)

Tactic:
exact H ⟨(Opens.map e.hom.base).obj U, hU.preimage_of_isIso e.hom⟩

Goal state after:
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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).OpenCover

Tactic:
apply
    (openCoverOfBase' 𝒰 f g).copy 𝒰.I₀
      (fun i =>
        pullback (pullback.snd _ _ : pullback f (𝒰.f i) ⟶ _)
          (pullback.snd _ _ : pullback g (𝒰.f i) ⟶ _))
      (fun i =>
        pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝒰.f i)
          pullback.condition.symm pullback.condition.symm)
      ((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit).symm) fun _ => Iso.refl _
  intro i
  rw [Iso.refl_hom, Category.id_comp, openCoverOfBase'_f]
  ext : 1 <;>
  · simp only [limit.lift_π, PullbackCone.mk_π_app, Equiv.trans_apply, Category.assoc,
    limit.lift_π_assoc, cospan_left, Category.comp_id,
      limit.isoLimitCone_inv_π_assoc, PullbackCone.π_app_left, IsPullback.cone_fst,
      pullbackSymmetry_hom_comp_snd_assoc, limit.isoLimitCone_inv_π,
      PullbackCone.π_app_right, IsPullback.cone_snd, pullbackSymmetry_hom_comp_fst_assoc]
    rfl

Goal state after: