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

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op)) r

Tactic:
← Functor.map_comp

Goal state after:
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ (ConcreteCategory.hom (X.toToΓSpecMapBasicOpen r)) r =
    (ConcreteCategory.hom (X.toRingedSpace.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op))) r
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ X.toSpecΓ ≫ Spec.map (Hom.appTop f) ≫ Y.isoSpec.inv = f

Tactic:
← Scheme.toSpecΓ_naturality_assoc,

Goal state after:
X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ ≫ Y.isoSpec.inv = f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| Spec.map (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
← Functor.map_comp

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
| Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map f) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι

Tactic:
← Functor.map_comp

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ Spec.map (X.presheaf.map ((eqToHom ⋯).op ≫ f)) ≫ (↑U).isoSpec.inv ≫ U.ι =
    Spec.map (X.presheaf.map ((homOfLE ⋯).op ≫ (eqToHom ⋯).op)) ≫ (↑U).isoSpec.inv ≫ U.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

pp: case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) (m : coequalizer f g ⟶ s.pt),
    coequalizer.π f g ≫ m = s.inl → (f ≫ coequalizer.π f g) ≫ m = s.inr → m = coequalizer.desc s.inl ⋯

Tactic:
· exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)

Goal state after:
case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) (m : coequalizer f g ⟶ s.pt),
    coequalizer.π f g ≫ m = s.inl → (f ≫ coequalizer.π f g) ≫ m = s.inr → m = coequalizer.desc s.inl ⋯
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 :
  Function.Bijective
    ⇑((algebraMap (↑((structurePresheafInCommRingCat R).stalk x))
          (Module.End ↑((structurePresheafInCommRingCat R).stalk x) ↑((structurePresheafInModuleCat R M).stalk x)))
        ((ConcreteCategory.hom (toStalk R x)) f))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ f • a = (ConcreteCategory.hom (toStalk R x)) f • a

Tactic:
toStalk_smul

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))
a : ↑((structurePresheafInModuleCat R M).stalk x)
⊢ f • a = f • a
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)
U : Opens ↑(PrimeSpectrum.Top R)
hxU : x ∈ U
s : ↑((structurePresheafInModuleCat R M).obj (op U))
g : R
hxg : x ∈ basicOpen g
igU : basicOpen g ≤ U
f : M
hs : const f g (basicOpen g) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map igU.hom.op)) s
⊢ (ConcreteCategory.hom (localizationtoStalkₗ R M x))
      ((ConcreteCategory.hom (openToLocalizationₗ R M (basicOpen g) x hxg)) (const f g (basicOpen g) ⋯)) =
    (ConcreteCategory.hom ((structurePresheafInModuleCat R M).germ (basicOpen g) x hxg))
      ((ConcreteCategory.hom ((structurePresheafInModuleCat R M).map igU.hom.op)) s)

Tactic:
refine (localizationtoStalkₗ_mk ..).trans
      congr((structurePresheafInModuleCat R M).germ _ x hxg $hs)

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen, ← Scheme.Hom.appTop]

Goal state after:
X : Scheme
r : ↑Γ(X, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appTop X.toSpecΓ)) ((ConcreteCategory.hom (ΓSpecIso Γ(X, ⊤)).inv) r)) =
    X.basicOpen r
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
⊢ D.Rel ⟨j, b⟩ ⟨k, c⟩ → D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
rintro ⟨y, e₃, e₄⟩

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩

Tactic:
have eq₂ : (pullback.snd _ _ : _ ⟶ D.V _) z = y := pullbackIsoProdSubtype_inv_snd_apply _ _ _

Goal state after:
D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
eq₁ : (ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z) = x
eq₂ : (ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z = y
⊢ D.Rel ⟨i, a⟩ ⟨k, c⟩
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j : D.J
U : Set ↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t i j ≫ D.f j i)) '' ⇑(ConcreteCategory.hom (D.f i j)) ⁻¹' U

Tactic:
convert! D.preimage_image_eq_image i j U using 1
  rw [coe_comp, coe_comp, Set.image_comp]
  congr! 1
  rw [← Set.eq_preimage_iff_image_eq, Set.preimage_preimage]
  · change _ = (D.t i j ≫ D.t j i ≫ _) ⁻¹' _
    rw [𝖣.t_inv_assoc]
  rw [bijective_iff_isIso_ofHom]
  apply (forget TopCat).map_isIso

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case right.left
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ IsOpen (⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x)))

pp: case right.right
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ x ∈ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))

Tactic:
· rw [← Set.image_preimage_eq_inter_range]
    apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap
    convert! hU (𝒰.idx x) using 1
    simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]
    congr! 1
    exact Set.preimage_image_eq _ 𝒰.fromGlued_injective

Goal state after:
case right.right
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ x ∈ ⇑(fromGlued 𝒰) '' U ∩ Set.range ⇑(𝒰.f (idx 𝒰 x))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf : ∀ (x y : 𝒰.I₀), pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y
x : 𝒰.I₀
⊢ 𝒰.f x ≫ glueMorphisms 𝒰 f hf = f x

Tactic:
by
  refine Cover.hom_ext (𝒰.ulift.pullback₁ (𝒰.f x)) _ _ fun i ↦ ?_
  dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, ulift_X, ulift_f, PreZeroHypercover.pullback₁_f]
  simp_rw [pullback.condition_assoc, ← ulift_f, ← ι_fromGlued, Category.assoc, glueMorphisms,
    IsIso.hom_inv_id_assoc, ulift_f, hf]
  simp [CategoryTheory.GlueData.ι]

Goal state after:
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 : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom (D.ι j).base) ⁻¹'
      ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U

Tactic:
←
    show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι j ≫ (D.gluedIso (forget C)).inv)) ⁻¹'
      ⇑(ConcreteCategory.hom ((D.mapGlueData (forget C)).ι i ≫ (D.gluedIso (forget C)).inv)) '' ↑U =
    ⇑(ConcreteCategory.hom (D.f j i).base) ''
      ⇑(ConcreteCategory.hom (D.t j i).base) ⁻¹' ⇑(ConcreteCategory.hom (D.f i j).base) ⁻¹' ↑U
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
h₁ : m ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i ≫ m =
    (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

Tactic:
dsimp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
    PreZeroHypercover.pullback₁_X, PullbackCone.mk_pt, PreZeroHypercover.pullback₁_f, gluing_ι]

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 ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = s.snd
i : (Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).I₀
⊢ pullback.fst s.fst (𝒰.f i) ≫ m =
    (pullbackSymmetry s.fst (𝒰.f i)).hom ≫
      pullback.map (𝒰.f i) s.fst (𝒰.f i ≫ f) g (𝟙 (𝒰.X i)) s.snd f ⋯ ⋯ ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i i).c.app (op U) ≫
      ((D.V (i, i)).presheaf.map (𝟙 (op ((Opens.map (D.f i i).base).obj U))) ≫ (D.V (i, i)).presheaf.map (eqToHom ⋯)) ≫
        invApp (D.f i i) ((Opens.map (D.t i i).base).1 ((Opens.map (D.f i i).base).obj U)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op =
    (D.U i).presheaf.map (eqToHom ⋯)

Tactic:
← Functor.map_comp

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
⊢ (D.f i i).c.app (op U) ≫
      (D.V (i, i)).presheaf.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫
        invApp (D.f i i) ((Opens.map (D.t i i).base).1 ((Opens.map (D.f i i).base).obj U)) ≫
          (D.U i).presheaf.map (eqToHom ⋯).op =
    (D.U i).presheaf.map (eqToHom ⋯)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).snd = s.snd

Tactic:
← cancel_mono (𝖣.ι j),

Goal state after:
case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ (lift (D.f i j) s.fst ⋯ ≫ (D.vPullbackCone i j).snd) ≫ D.ι j = s.snd ≫ D.ι j
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
⊢ Ideal.span (Set.range (mulNumerator s p)) = ⊤

Tactic:
rw [← Ideal.radical_eq_top, eq_top_iff, ← hsone, Ideal.span_le]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
s : Set R
hsone : Ideal.span s = ⊤
Rₜ : ↑s → Type u_2
inst✝² : (t : ↑s) → CommRing (Rₜ t)
inst✝¹ : (t : ↑s) → Algebra R (Rₜ t)
inst✝ : ∀ (t : ↑s), Away (↑t) (Rₜ t)
p : (t : ↑s) → Set (Rₜ t)
htone : ∀ (r : ↑s), Ideal.span (p r) = ⊤
⊢ s ⊆ ↑(Ideal.span (Set.range (mulNumerator s p))).radical
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
locally_iff_exists hPi

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
⊢ ∃ ι s,
    ∃ (_ : Ideal.span (Set.range s) = ⊤),
      ∃ Sₜ x x_1,
        ∃ (_ : ∀ (i : ι), IsLocalization.Away (s i) (Sₜ i)), ∀ (i : ι), P ((algebraMap T (Sₜ i)).comp (g.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case h₂
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)

Tactic:
· introv H U
    rw [Scheme.Hom.comp_appLE, CommRingCat.hom_comp, h₁.cancel_left_isIso]
    exact H U

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

Goal state before:
pp: case of_basicOpenCover
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ ∀ {X Y : Scheme} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ →
      (∀ (r : ↥s), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ Y.basicOpen ↑r)) →
        sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
· introv hs hs' U
    apply h₃ _ _ hs
    intro r
    simp_rw [sourceAffineLocally_morphismRestrict] at hs'
    have := hs' r ⟨X.basicOpen (f.appLE ⊤ U le_top r.1), U.2.basicOpen (f.appLE ⊤ U le_top r.1)⟩
      (by simp [Scheme.Hom.appLE])
    rwa [IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2, CommRingCat.hom_ofHom,
      ← h₁.isLocalization_away_iff] at this

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ CompactSpace ↥(pullback f g)

Tactic:
have : Finite 𝒰.I₀ := by dsimp [𝒰]; infer_instance

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
this✝ : AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X :=
  HasAffineProperty.isLocal_affineProperty @QuasiCompact
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite 𝒰.I₀
⊢ CompactSpace ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H : P f
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
rw [eq_affineLocally P, affineLocally_iff_affineOpens_le] at H

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
U : ↑Y.affineOpens
V : ↑X.affineOpens
e : ↑V ≤ f ⁻¹ᵁ ↑U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.height = ⨅ J ∈ I.minimalPrimes, J.height

Tactic:
apply iInf_congr (fun p ↦ iInf_congr fun hp ↦ ?_)
  have := hp.isPrime
  exact (Ideal.height_eq_primeHeight _).symm

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
p : Ideal R
hp : p ∈ (J ⊔ span {x}).minimalPrimes
this✝¹ : p.IsPrime
h✝ : ¬p.height = ⊤
this✝ : p.FiniteHeight
this : J.height ≤ p.height
h : ↑r ≠ p.height
⊢ ↑(r + 1) ≤ p.height

Tactic:
by
        exact Order.add_one_le_of_lt (lt_of_le_of_ne (h₃.trans this) h)

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

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x - (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y = 0 → ∃ c, ↑c * x = ↑c * y

Tactic:
← map_sub,

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
x : ↥X
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

Tactic:
wlog h : ∃ R, X = Spec R
  · obtain ⟨R, f, hf, hsub⟩ := Scheme.exists_affine_mem_range_and_range_subset
      (show x ∈ ⊤ from trivial)
    obtain ⟨y, rfl⟩ := Set.mem_range.mp hsub.1
    rw [coheight_eq_of_isOpenImmersion, ← this _ ⟨R, rfl⟩]
    exact Order.krullDim_eq_of_orderIso
      (PrimeSpectrum.comapEquiv (asIso (Scheme.Hom.stalkMap f y)).commRingCatIsoToRingEquiv)
  obtain ⟨R, rfl⟩ := h
  let k : Algebra ↑R ↑((Spec R).presheaf.stalk x) := StructureSheaf.stalkAlgebra (↑R) x
  have : IsLocalization.AtPrime (↑((Spec R).presheaf.stalk x)) x.asIdeal :=
    StructureSheaf.IsLocalization.to_stalk R x
  rw [IsLocalization.AtPrime.ringKrullDim_eq_height x.asIdeal ((Spec R).presheaf.stalk x)]
  apply WithBot.coe_eq_coe.mpr
  exact idealHeight_eq_coheight R x

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

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op)) I =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I

Tactic:
← Functor.map_comp

Goal state after:
X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) I =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I