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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
⊢ basicOpen (g i * g j) ≤ U

Tactic:
exact ((PrimeSpectrum.basicOpen_mul (g i) (g j)).trans_le inf_le_right).trans (igU _)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ e.inv ≫ g = pullback.snd f g ≫ g

Tactic:
IsOpenImmersion.isoOfRangeEq_inv_fac,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y U : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
V : Y.Opens := Scheme.Hom.opensRange g
e : U ≅ ↑V := IsOpenImmersion.isoOfRangeEq g V.ι ⋯
t : pullback f g ⟶ pullback f V.ι := pullback.map f g f V.ι (𝟙 X) e.hom (𝟙 Y) ⋯ ⋯
⊢ t ≫ (pullbackRestrictIsoRestrict f V).hom ≫ f ∣_ Scheme.Hom.opensRange g ≫ V.ι = pullback.snd f g ≫ g
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit D Scheme.Γ.rightOp

Tactic:
suffices PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp from
    preservesLimit_of_iso_diagram _ (asIso α).symm

Goal state after:
I : Type w
inst✝¹ : Category.{v, w} I
D : I ⥤ Scheme
inst✝ : ∀ (i : I), IsAffine (D.obj i)
α : D ⟶ (D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
this✝ : ∀ (i : I), IsIso (α.app i)
this : IsIso α
⊢ PreservesLimit ((D ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec) Scheme.Γ.rightOp
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
⊢ ∀ {i j k : Discrete J} (fi : i ⟶ k) (fj : j ⟶ k) (xi : F.obj i) (xj : F.obj j),
    (ConcreteCategory.hom (F.map fi)) xi = (ConcreteCategory.hom (F.map fj)) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨k⟩ ⟨⟨⟨⟩⟩⟩ ⟨⟨⟨⟩⟩⟩

Goal state after:
J : Type u_1
inst✝ : Category.{v_1, u_1} J
F : Discrete J ⥤ Type u_2
i : J
⊢ ∀ (xi xj : F.obj { as := i }),
    (ConcreteCategory.hom (F.map { down := { down := ⋯ } })) xi =
        (ConcreteCategory.hom (F.map { down := { down := ⋯ } })) xj →
      ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xj
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: R : CommRingCat
⊢ Spec.map (Scheme.ΓSpecIso R).inv ≫ (Spec R).toSpecΓ = 𝟙 (Spec Γ(Spec R, ⊤))

Tactic:
by
  rw [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Iso.hom_inv_id, Spec.map_id]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v, u₁} C
C' : Type u₂
inst✝¹ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ F.map (D.t i i) = 𝟙 (F.obj (D.V (i, i)))

Tactic:
by
    simp

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : i = k
⊢ IsIso (pullback.snd (D.f' j k) (D.f' j i))

Tactic:
subst hik; infer_instance

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case h
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
h₂ :
  D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.t i k ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
⊢ (ConcreteCategory.hom (D.f i k))
        ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z)) =
      (ConcreteCategory.hom (D.f i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z)) ∧
    (ConcreteCategory.hom (D.f k i))
        ((ConcreteCategory.hom (D.t i k))
          ((ConcreteCategory.hom (pullback.fst (D.f i k) (D.f i j))) ((ConcreteCategory.hom (D.t' j i k)) z))) =
      (ConcreteCategory.hom (D.f k j))
        ((ConcreteCategory.hom (D.t j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z))

Tactic:
exact ⟨CategoryTheory.congr_fun h₁ z, CategoryTheory.congr_fun h₂ z⟩

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((f.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((g.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s)

Tactic:
SheafedSpace.congr_hom_app (coequalizer.condition f.toShHom g.toShHom),

Goal state after:
case H
X Y : LocallyRingedSpace
f g : X ⟶ Y
U : Opens ↑↑(coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
s : ↑((coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.obj (op U))
⊢ X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          ((Hom.toShHom g ≫ coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
            X.presheaf.map (eqToHom ⋯)))
        s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom ((g.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case h
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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (pullback.fst (D.f k i) (D.f k j)).c.app
          (op ((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯) ≫
          (pullback (D.f k i) (D.f k j)).presheaf.map ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op ≫
            invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U)

Tactic:
IsOpenImmersion.inv_naturality,

Goal state after:
case h
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))
⊢ (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯) =
    (D.t k i).c.app (op ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U)) ≫
      (pullback.fst (D.f k i) (D.f k j)).c.app
          (op ((Opens.map (D.t k i).base).obj ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U))) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯) ≫
          invApp (pullback.fst (D.f k i) (D.f k j))
              (unop
                (op
                  ((Opens.map (D.t' k i j).base).obj
                    ((Opens.map (pullback.snd (D.f i j) (D.f i k)).base).obj
                      ((opensFunctor (pullback.snd (D.f i j) (D.f i k))).obj U))))) ≫
            (D.V (k, i)).presheaf.map
              ((opensFunctor (pullback.fst (D.f k i) (D.f k j))).op.map
                ((Opens.map (D.t' k i j).base).map (eqToHom ⋯).unop).op)
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 α
this : α z = x
⊢ ∃ l fi fj fk α z,
    IsOpenImmersion α ∧
      α ≫ pullback.fst (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧
        α ≫ pullback.snd (V F i j).ι (V F i k).ι = (Hom.isoOpensRange (F.map fi)).hom ≫ (F.obj i).homOfLE ⋯ ∧ α z = x

Tactic:
exact ⟨l, hli ≫ k₁.2.1, hli ≫ k₁.2.2, hlk ≫ k₂.2.2, α, z, ‹_›, by simp [α], by simp [α], ‹_›⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥(X ⨿ Y)
⊢ x ∈
    Set.range
      ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
              f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) ((coprodMk X Y).symm x)))

Tactic:
obtain ⟨x, rfl⟩ := (coprodMk X Y).surjective x

Goal state after:
case h
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
x : ↥X ⊕ ↥Y
⊢ (coprodMk X Y) x ∈
    Set.range
      ⇑({ I₀ := PUnit.{w + 1} ⊕ PUnit.{w + 1}, X := fun x ↦ Sum.elim (fun x ↦ X) (fun x ↦ Y) x,
              f := fun x ↦ Sum.rec (fun x ↦ coprod.inl) (fun x ↦ coprod.inr) x }.f
          (Sum.elim (fun x ↦ Sum.inl PUnit.unit) (fun x ↦ Sum.inr PUnit.unit) ((coprodMk X Y).symm ((coprodMk X Y) x))))
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) ⋯
this✝ : IsOpenImmersion α
this : α y = x
⊢ ∃ 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:
refine ⟨α.opensRange, ⟨y, this⟩, ?_⟩

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 α
this : α y = x
⊢ (Hom.opensRange α).ι ≫
      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 =
    (Hom.opensRange α).ι ≫
      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.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:
intro X' Y' αX αY f h₁ h₂
      have h₁' (x : _) := congr($h₁ x).symm
      have h₂' (x : _) := congr($h₂ x).symm
      dsimp at h₁ h₂ h₁' h₂'
      refine ⟨(IsOpenImmersion.isPullback _ _ _ _ h₁.symm ?_).flip,
        (IsOpenImmersion.isPullback _ _ _ _ h₂.symm ?_).flip⟩ <;>
        ext x <;> obtain ⟨x | x, rfl⟩ := (coprodMk _ _).surjective x <;> simp_all

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ Hom.opensRange ι₁ ⊓ U ⊔ Hom.opensRange ι₂ ⊓ U = U

Tactic:
← inf_sup_right,

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
U : (X ⨿ Y).Opens
ι₁ : X ⟶ X ⨿ Y := coprod.inl
ι₂ : Y ⟶ X ⨿ Y := coprod.inr
⊢ (Hom.opensRange ι₁ ⊔ Hom.opensRange ι₂) ⊓ U = 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 : PullbackCone f g
i : 𝒰.I₀
⊢ Multicoequalizer.π (gluing 𝒰 f g).diagram i ≫
      Multicoequalizer.desc (gluing 𝒰 f g).diagram X (fun i ↦ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) ⋯ =
    pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i

Tactic:
Multicoequalizer.π_desc

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
i : 𝒰.I₀
⊢ pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i = pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i
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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          D.diagramOverOpenπ U j ≫
            (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
                (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
              𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
limit.w_assoc

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)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
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
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
this :
  IsPullback (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
⊢ (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) ≫ 𝟙 Z = 𝟙 (pullback f (𝒰.f i)) ≫ (Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f

pp: case refine_2
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
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
this :
  IsPullback (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
· simp [← pullback.condition]

Goal state after:
case refine_2
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
i : (openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).I₀
this :
  IsPullback (pullback.snd (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)))
    (pullback.fst (pullback.snd g (𝒰.f i)) (pullback.snd f (𝒰.f i)) ≫ pullback.fst g (𝒰.f i))
    (pullback.snd f (𝒰.f i) ≫ 𝒰.f i) g
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
obtain ⟨s', h₁, h₂⟩ := (Ideal.span_eq_top_iff_finite s).mp hsone

Goal state after:
case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
s' : Finset S
h₁ : ↑s' ⊆ s
h₂ : Ideal.span ↑s' = ⊤
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
← IsScalarTower.algebraMap_eq

Goal state after:
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
e : S ≃ₐ[R] Localization.Away 1 := AlgEquiv.restrictScalars R (IsLocalization.atUnits S (Submonoid.powers 1) ⋯)
this : IsLocalization.Away r (Localization.Away 1)
⊢ P (algebraMap R (Localization.Away 1))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P
    (((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
          (algebraMap S (Localization.Away a))).comp
      f)

Tactic:
comp_assoc

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra S T
t : S
inst✝ : IsLocalization.Away t T
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
a : S
ha : a ∈ s
this✝ : Algebra (Localization.Away a) (Localization.Away ((algebraMap S T) a)) :=
  (IsLocalization.Away.map (Localization.Away a) (Localization.Away ((algebraMap S T) a)) (algebraMap S T) a).toAlgebra
this :
  (algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      (algebraMap S (Localization.Away a)) =
    (algebraMap T (Localization.Away ((algebraMap S T) a))).comp (algebraMap S T)
⊢ P
    ((algebraMap (Localization.Away a) (Localization.Away ((algebraMap S T) a))).comp
      ((algebraMap S (Localization.Away a)).comp f))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : FiniteRingKrullDim R
⊢ ∃ p, p.IsMaximal ∧ ↑p.height = ringKrullDim R

Tactic:
by
  let l := LTSeries.longestOf (PrimeSpectrum R)
  obtain ⟨m, hm, hle⟩ := l.last.asIdeal.exists_le_maximal IsPrime.ne_top'
  refine ⟨m, hm, le_antisymm (height_le_ringKrullDim_of_ne_top IsPrime.ne_top') ?_⟩
  trans (l.last.asIdeal.height : WithBot ℕ∞)
  · rw [Ideal.height_eq_primeHeight]
    exact LTSeries.height_last_longestOf.symm.le
  · norm_cast
    exact height_mono hle

Goal state after: