mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x✝ : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x✝ ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
Vb : Opens ↑(PrimeSpectrum.Top R)
mb : ↑x✝ ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
x : ↥(Va ⊓ Vb)
hsax : sa ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsa : (fun x ↦ a (ia x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk ra ⟨sa, hsax⟩
⊢ ∃ (hs : sa * sb ∉ (↑x).asIdeal),
    (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) x = LocalizedModule.mk (ra * rb) ⟨sa * sb, hs⟩

Tactic:
obtain ⟨hsbx, hsb⟩ := wb ⟨x.1, x.2.2⟩

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
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
a b : (x : ↥U) → Localizations A ↑x
ha : a ∈ (sectionsSubmodule A U).carrier
hb : b ∈ (sectionsSubmodule A U).carrier
x✝ : ↥U
Va : Opens ↑(PrimeSpectrum.Top R)
ma : ↑x✝ ∈ Va
ia : Va ⟶ U
ra : A
sa : R
wa : ∀ (x : ↥Va), ∃ (hs : sa ∉ (↑x).asIdeal), (fun x ↦ a (ia x)) x = LocalizedModule.mk ra ⟨sa, hs⟩
Vb : Opens ↑(PrimeSpectrum.Top R)
mb : ↑x✝ ∈ Vb
ib : Vb ⟶ U
rb : A
sb : R
wb : ∀ (x : ↥Vb), ∃ (hs : sb ∉ (↑x).asIdeal), (fun x ↦ b (ib x)) x = LocalizedModule.mk rb ⟨sb, hs⟩
x : ↥(Va ⊓ Vb)
hsax : sa ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsa : (fun x ↦ a (ia x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk ra ⟨sa, hsax⟩
hsbx : sb ∉ (↑⟨↑x, ⋯⟩).asIdeal
hsb : (fun x ↦ b (ib x)) ⟨↑x, ⋯⟩ = LocalizedModule.mk rb ⟨sb, hsbx⟩
⊢ ∃ (hs : sa * sb ∉ (↑x).asIdeal),
    (fun x ↦ (a * b) ((Va.infLELeft Vb ≫ ia) x)) x = LocalizedModule.mk (ra * rb) ⟨sa * sb, hs⟩
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (X.presheaf.map (homOfLE ⋯).op)

Tactic:
change IsIso (X.presheaf.map (eqToIso U.ι_image_top).hom.op)

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
U : X.Opens
⊢ IsIso (X.presheaf.map (eqToIso ⋯).hom.op)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ const f g₁ U hu₁ * const g₁ g₂ U hu₂ = const f g₂ U hu₂

Tactic:
rw [const_mul, const_ext]

Goal state after:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ • (f * g₁) = (g₁ * g₂) • f
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
obtain ⟨S, hS, hxS, hSU⟩ := X.affineBasisCover_is_basis.exists_subset_of_mem_open hU U.isOpen

Goal state after:
X : Scheme
U : TopologicalSpace.Opens ↥X
x : ↥X
hU : x ∈ ↑U
S : Set ↥X
hS : S ∈ {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
hxS : x ∈ S
hSU : S ⊆ ↑U
⊢ ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
y : Y
hy : y ∈ U
e' :
  (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) y) =
    (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) x✝)
e'' : Function.Injective ⇑(hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
⊢ x✝ ∈ U

Tactic:
refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem y _ (Quot.eqvGen_exact ?_))).mp hy

Goal state after:
case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
y : Y
hy : y ∈ U
e' :
  (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) y) =
    (hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
      ((hom (Cofork.π (coequalizerColimit f g).cocone)) x✝)
e'' : Function.Injective ⇑(hom (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv)
⊢ Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) y = Quot.mk (Function.Coequalizer.Rel ⇑(hom f) ⇑(hom g)) x✝
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mpr
D : GlueData
i j : D.J
x : ↑(D.U i)
y : ↑(D.U j)
⊢ D.Rel ⟨i, x⟩ ⟨j, y⟩ → (ConcreteCategory.hom (D.ι i)) x = (ConcreteCategory.hom (D.ι j)) y

Tactic:
rintro ⟨z, e₁, e₂⟩
    dsimp only at *
    -- Porting note: there were `subst e₁` and `subst e₂`, instead of the `rw`
    rw [← e₁, ← e₂] at *
    rw [D.glue_condition_apply]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D : GlueData
i : D.J
⊢ ((D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.ι i ≫
          D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace.inv) ≫
        (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base

Tactic:
D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι_isoPresheafedSpace_inv i

Goal state after:
D : GlueData
i : D.J
⊢ ((D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i).hom ≫
        (D.toLocallyRingedSpaceGlueData.isoSheafedSpace.inv ≫
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
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 : (pullback.snd (D.f i j) (D.f i k)).base = (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U

Tactic:
replace this := congr_arg (TopCat.Hom.hom ·) this

Goal state after:
case w
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 (inv (D.t' k i j) ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i).base
⊢ ⇑(ConcreteCategory.hom (D.t k i).base) ⁻¹' ⇑(ConcreteCategory.hom (pullback.snd (D.f i j) (D.f i k)).base) '' ↑U =
    ⇑(ConcreteCategory.hom (pullback.fst (D.f k i) (D.f k j)).base) '' ⇑(ConcreteCategory.hom (D.t' k i j).base) ⁻¹' ↑U
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
by apply pullback.hom_ext <;> simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

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

Tactic:
rw [Category.id_comp]

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

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

Tactic:
rw [Category.id_comp]

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

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

Tactic:
rw [Category.id_comp]

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

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

Tactic:
rw [Category.id_comp]

Goal state after:
case h₁
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
i j k : 𝒰.I₀
⊢ (t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j) ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)
Module: Mathlib.AlgebraicGeometry.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)
i : J
⊢ ⊤ ≤ Hom.opensRange (F.map ⟨i, (𝟙 i, 𝟙 i)⟩.snd.1)

Tactic:
by simp [Scheme.Hom.opensRange_of_isIso]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: A : Scheme
f : A ⟶ ⊥_ Scheme
⊢ IsIso f

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ ⟨i, x⟩ = ⟨j, y⟩ → ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y

Tactic:
simp only [Discrete.functor_obj_eq_as, Sigma.mk.injEq]

Goal state after:
case refine_2
σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i j : σ
x : ↥(g i)
y : ↥(g j)
⊢ i = j ∧ x ≍ y → ∃ k fi fj x_1, ((Discrete.functor g).map fi) x_1 = x ∧ ((Discrete.functor g).map fj) x_1 = y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g✝ : σ → Scheme
inst✝ : Small.{u, v} σ
g : σ → Scheme
i j : σ
hij : i ≠ j
⊢ IsEmpty ↥(pullback.cone (Sigma.ι g i) (Sigma.ι g j)).pt

Tactic:
exact isEmpty_pullback_sigmaι_of_ne _ hij

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 : D.J
U : Opens ↑↑(D.U i)
X Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
f' : X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop X) ≫ (D.diagramOverOpen U).map f'

Tactic:
induction X with | op X => ?_

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
Y : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
X : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop Y) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map 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
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_

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
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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 ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).fst = s.fst
h₂ : m ≫ (PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯).snd = s.snd
⊢ m = gluedLift 𝒰 f g s

Tactic:
simp_rw [PullbackCone.mk_pt, PullbackCone.mk_π_app] at h₁ 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 ≫ p1 𝒰 f g = s.fst
h₂ : m ≫ p2 𝒰 f g = 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✝ 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

Tactic:
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]

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.snd m (pullback.fst (p1 𝒰 f g) (𝒰.f i)) ≫ pullback.fst (p1 𝒰 f g) (𝒰.f i) =
    ((pullbackRightPullbackFstIso (p1 𝒰 f g) (𝒰.f i) m).hom ≫
        pullback.map (m ≫ p1 𝒰 f g) (𝒰.f i) s.fst (𝒰.f i) (𝟙 s.pt) (𝟙 (𝒰.X i)) (𝟙 X) ⋯ ⋯) ≫
      (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.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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
⊢ ⊤ ≤ Hom.opensRange (F.map ⟨↓i, (𝟙 ↓i, f)⟩.snd.1)

Tactic:
by simp [Scheme.Hom.opensRange_of_isIso]

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

Goal state before:
pp: case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))

Tactic:
rw [Category.id_comp]

Goal state after:
case op.right
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j : (MultispanShape.prod D.J).R
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))
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)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (Localization.awayMap g' ↑a) ((algebraMap S (Localization.Away ↑a)) (f x))

Tactic:
simp only [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_eq]

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)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (algebraMap (Localization.Away ↑b) (Localization.Away (g' ↑a))) (g' (f x))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP :
  ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β)
    (g : β → γ), P f → P g → P (g ∘ f)
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) f
hg : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) g
⊢ P (⇑g ∘ ⇑f)

Tactic:
exact hP _ _ hf hg

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
this : Finite 𝒰.I₀
⊢ CompactSpace ↥(pullback f g)

Tactic:
have : ∀ i, CompactSpace (𝒰.X i) := by intro i; 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₀
this : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
⊢ CompactSpace ↥(pullback f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst✝ : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (⇑f '' Z)
this :
  ∀ {X : Scheme} (S : CommRingCat) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X),
    IsClosed Z → StableUnderSpecialization (⇑f '' Z) → (∃ R, X = Spec R) → IsClosed (⇑f '' Z)
hX : ¬∃ R, X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective ⇑g
⊢ CompactSpace ↥(Spec R)

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ (algebraMap R S) y = 0

Tactic:
IsLocalization.map_eq_zero_iff M

Goal state after:
case succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : y * ↑m' = 0
⊢ ∃ m, ↑m * y = 0
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
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)

Tactic:
have H := (isLocal_ringHomProperty P).respectsIso
  rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]

Goal state after:
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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ P (𝟙 X ∣_ ↑U)

Tactic:
rw [morphismRestrict_id, iff_of_isAffine (P := P), Scheme.Hom.id_appTop]

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
hP : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : ↑X.affineOpens
this : IsAffine ↑(𝟙 X ⁻¹ᵁ ↑U)
⊢ Q (CommRingCat.Hom.hom (𝟙 Γ(↑(𝟙 X ⁻¹ᵁ ↑U), ⊤)))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
⊢ Order.height { asIdeal := p, isPrime := inst✝ } ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n

Tactic:
Order.height_le_coe_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
⊢ (∀ y < { asIdeal := p, isPrime := inst✝ }, Order.height y < ↑n) ↔ ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n