mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := fun i ↦ ↑(sf i)
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ ∃ V, ∃ (_ : ↑⟨x, mem⟩ ∈ V), ∃ i, P.pred fun x ↦ gl (i x)

Tactic:
use U i, hi, Opens.leSupr U i

Goal state after:
case h
X : TopCat
T : ↑X → Type u_1
P : LocalPredicate T
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((subpresheafToTypes P.toPrelocalPredicate).obj (op (U i)))
sf_comp : (subpresheafToTypes P.toPrelocalPredicate).IsCompatible U sf
sf' : (i : ι) → (X.presheafToTypes T).obj (op (U i)) := ⋯
sf'_comp : (X.presheafToTypes T).IsCompatible U sf'
gl : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))
gl_spec : IsGluing (X.sheafToTypes T).obj U sf' gl
gl_uniq :
  ∀ (y : ToType ((X.sheafToTypes T).obj.obj (op (iSup U)))),
    (fun s ↦ IsGluing (X.sheafToTypes T).obj U sf' s) y → y = gl
x : ↑X
mem : x ∈ unop (op (iSup U))
i : ι
hi : x ∈ U i
⊢ P.pred fun x ↦ gl ((Opens.leSupr U i) x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

pp: case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c

Tactic:
· exact Spec.topMap_comp f g

Goal state after:
case h
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj T).presheaf =
    (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
intro x hx
  have hxU : x ∈ U := X.basicOpen_le _ hx
  simp_rw [← SetLike.mem_coe, Opens.coe_sup, Set.mem_union, SetLike.mem_coe] -- TODO : Opens.mem_sup
  simp only [Scheme.mem_basicOpen _ _ _ hxU, map_add] at hx ⊢
  exact IsLocalRing.isUnit_or_isUnit_of_isUnit_add hx

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s : PullbackCone f g
U V : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
i : U ⟶ V
⊢ (pullbackConeOfLeft f g).pt.presheaf.map i ≫ s.snd.c.app (⋯.functor.op.obj V) ≫ s.pt.presheaf.map (eqToHom ⋯) =
    (s.snd.c.app (⋯.functor.op.obj U) ≫ s.pt.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.lift s.fst.base s.snd.base ⋯)).obj s.pt.presheaf).map i

Tactic:
by
        erw [s.snd.c.naturality_assoc]
        rw [Category.assoc]
        erw [← s.pt.presheaf.map_comp, ← s.pt.presheaf.map_comp]
        congr 1

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ limit.cone (cospan f.base g.base) ≅
    (Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj ((forget C).mapCone (pullbackConeOfLeft f g))

Tactic:
fapply Cone.ext

Goal state after:
case φ
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (limit.cone (cospan f.base g.base)).pt ≅
    ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
        ((forget C).mapCone (pullbackConeOfLeft f g))).pt

case w
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ autoParam
    (∀ (j : WalkingCospan),
      (limit.cone (cospan f.base g.base)).π.app j =
        Iso.hom ?φ ≫
          ((Cone.postcompose (diagramIsoCospan (cospan f g ⋙ forget C)).hom).obj
                  ((forget C).mapCone (pullbackConeOfLeft f g))).π.app
            j)
    Cone.ext._auto_1
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
⊢ IsCompact (⋃ i, Set.range ⇑(𝒰.f i))

Tactic:
apply isCompact_iUnion

Goal state after:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
val✝ : Fintype 𝒰.I₀
⊢ ∀ (i : 𝒰.I₀), IsCompact (Set.range ⇑(𝒰.f i))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
W : (↑U).Opens
⊢ U.ι ''ᵁ W ≤ U

Tactic:
simp_rw [← U.ι_image_top]
  exact U.ι.image_mono le_top

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen
      ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op))
        ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op)) r))

Tactic:
← CommRingCat.comp_apply,

Goal state after:
X : Scheme
U : X.Opens
r : ↑Γ(↑U, ⊤)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appIso (X.ofRestrict ⋯) ⊤).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (X.presheaf.map (eqToHom ⋯).op ≫ X.presheaf.map (eqToHom ⋯).op)) r)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ U.ι = (Iso.refl ↑U).hom ≫ U.ι

Tactic:
Iso.refl_hom,

Goal state after:
X : Scheme
U : X.Opens
⊢ U.ι = 𝟙 ↑U ≫ U.ι
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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

Tactic:
← CommRingCat.comp_apply,

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: ⊢ PreservesLimitsOfSize.{u_1, u_1, u_1, u_1, u_1 + 1, u_1 + 1}
    ((equivCommRingCat.functor ⋙ equivCommRingCat.inverse) ⋙ forgetToScheme)

Tactic:
change PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)

Goal state after:
⊢ PreservesLimits (equivCommRingCat.functor ⋙ Scheme.Spec)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) ⁻¹' U)

Tactic:
← Multicoequalizer.ι_sigmaπ 𝖣.diagram

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤

Tactic:
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ ↔ Ideal.span s = ⊤
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.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        ((ConcreteCategory.hom ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U))) s))

Tactic:
← CommRingCat.comp_apply,

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 ((f.toHom ≫ (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom).c.app (op U))) s) =
    X.toRingedSpace.basicOpen
      ((ConcreteCategory.hom
          ((coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.c.app (op U) ≫
            g.c.app (op ((Opens.map (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base).1 U))))
        s)
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) =
    Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom)

Tactic:
← cancel_mono φ,

Goal state after:
case e_a
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ : Function.Injective ⇑(ConcreteCategory.hom φ)
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Spec.homEquiv (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ =
    Spec.homEquiv (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
x : ↑↑(Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).toPresheafedSpace
⊢ IsLocalRing ↑((Limits.coequalizer (Hom.toShHom f) (Hom.toShHom g)).presheaf.stalk x)

Tactic:
by
    obtain ⟨y, rfl⟩ :=
      (TopCat.epi_iff_surjective (coequalizer.π f.toShHom g.toShHom).hom.base).mp inferInstance x
    exact ((coequalizer.π f.toShHom g.toShHom :).hom.stalkMap y).hom.domain_isLocalRing

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
J : Type u
U : J → Opens α
⊢ Function.Injective ⇑(ConcreteCategory.hom (fromOpenSubsetsGlue U))

Tactic:
intro x y e
  obtain ⟨i, ⟨x, hx⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective x
  obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y
  rw [ι_fromOpenSubsetsGlue_apply, ι_fromOpenSubsetsGlue_apply] at e
  subst e
  rw [(ofOpenSubsets U).ι_eq_iff_rel]
  exact ⟨⟨⟨x, hx⟩, hy⟩, rfl, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: X : Scheme
inst✝ : IsEmpty ↥X
U : X.Opens
⊢ Subsingleton ↑Γ(X, U)

Tactic:
by
  obtain rfl : U = ⊥ := Subsingleton.elim _ _; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
g : σ → Scheme
inst✝ : Small.{u, v} σ
i : σ
U : (∐ g).Opens
hU : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
x : ↥(g i)
hx : (Sigma.ι g i) x ∈ U
h : i ≠ i
hU' : U ≤ Scheme.Hom.opensRange (Sigma.ι g i)
hy : (Sigma.ι g i) x = (Sigma.ι g i) x
⊢ (Sigma.ι g i) x ∈ ⊥

Tactic:
cases h rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
rintro ⟨ix, x⟩ ⟨iy, y⟩ e

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

Goal state before:
pp: case right.refine_1
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ (Sigma.desc α)
      (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y) =
    (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

pp: case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y

Tactic:
· simp [← Scheme.Hom.comp_apply]

Goal state after:
case right.refine_2
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
x : ↥(∐ f)
y :
  ↥((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).X
      (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
hy :
  ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
        (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
      y =
    x
⊢ Scheme.Hom.stalkMap (Sigma.desc α)
        (((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
            (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
          y) ≫
      Scheme.Hom.stalkMap
        ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f
          (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x))
        y =
    (X.presheaf.stalkCongr ⋯).hom ≫
      Scheme.Hom.stalkMap (α (Scheme.Cover.idx (Scheme.IsLocallyDirected.openCover (Discrete.functor f)) x).as) y
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫ prod.fst) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))

Tactic:
limit.isoLimitCone_inv_π

Goal state after:
case h₁
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.left }) =
    Spec.map (CommRingCat.ofHom (RingHom.fst ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫ prod.snd) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))

Tactic:
limit.isoLimitCone_inv_π

Goal state after:
case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ Spec.map ({ cone := R.prodFan S, isLimit := R.prodFanIsLimit S }.cone.π.app { as := WalkingPair.right }) =
    Spec.map (CommRingCat.ofHom (RingHom.snd ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
s : Set σ
hs : s.Finite
U : σ → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
hU' : s.Pairwise (Disjoint on U)
⊢ IsAffineOpen (⨆ i ∈ s, U i)

Tactic:
rw [← iSup_subtype'']
  have := hs.to_subtype
  exact .iSup_of_disjoint (by simpa) fun i j e ↦ hU' i.2 j.2 (by aesop)

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:
P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)

Goal state after:
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))
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀), P ((Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i ≫ f)
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
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
⊢ (precoverage IsOpenImmersion).ZeroHypercover ((openCoverOfLeft (Precoverage.ZeroHypercover.pullback₁ f 𝒰) f g).X i)

Tactic:
refine
    @coverOfIsIso _ _ _ _ _
      (f := (pullbackSymmetry (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))).hom ≫
        (limit.isoLimitCone ⟨_, this.isLimit⟩).inv ≫
        pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance

Goal state after:
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

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.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
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    (Iso.refl (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)))).hom ≫
      (openCoverOfBase' 𝒰 f g).f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) i)

Tactic:
Iso.refl_hom,

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✝
𝒰 : Z.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
i : 𝒰.I₀
⊢ pullback.map (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i)) f g (pullback.fst f (𝒰.f i)) (pullback.fst g (𝒰.f i))
      (𝒰.f i) ⋯ ⋯ =
    𝟙 (pullback (pullback.snd f (𝒰.f i)) (pullback.snd g (𝒰.f i))) ≫
      (openCoverOfBase' 𝒰 f g).f (((Equiv.prodPUnit 𝒰.I₀).symm.trans (Equiv.sigmaEquivProd 𝒰.I₀ PUnit.{v + 1}).symm) 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
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
⊢ (((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom) ≫ (F.obj ↓i).homOfLE ⋯) ≫
      tAux F (↓i) ↓j ≫ (glueData F).ι j =
    tAux F (↓i) ↓j ≫ (glueData F).ι j

Tactic:
convert! Category.id_comp _

Goal state after:
case e'_2.e'_6
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
this✝ : IsIso (V F (↓i) ↓j).ι
this : tAux F (↓i) ↓j ≫ (glueData F).ι j = (V F (↓i) ↓j).ι ≫ (glueData F).ι i
e_4✝ : ↑(⨆ k, Hom.opensRange (F.map k.snd.1)) = ↑(V F (↓i) ↓j)
⊢ ((V F (↓i) ↓j).ι ≫ (Hom.isoOpensRange (F.map (𝟙 ↓i))).hom) ≫ (F.obj ↓i).homOfLE ⋯ = 𝟙 ↑(V F (↓i) ↓j)
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).fst ≫ D.ι i = s.snd ≫ D.ι j

Tactic:
conv_rhs => rw [← s.condition]

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).fst ≫ D.ι i = s.fst ≫ D.ι i
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) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ x ∈ ↑(Ideal.span (⇑(algebraMap R (Rₜ ⟨a, ha⟩)) '' Set.range (mulNumerator s p)))

Tactic:
rw [SetLike.mem_coe, IsLocalization.mem_span_map (Submonoid.powers a)]

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) = ⊤
a : R
ha : a ∈ s
this : IsLocalization (Submonoid.powers a) (Rₜ ⟨a, ha⟩)
x : Rₜ ⟨a, ha⟩
hx : x ∈ p ⟨a, ha⟩
⊢ ∃ y ∈ Ideal.span (Set.range (mulNumerator s p)), ∃ z, x = mk' (Rₜ ⟨a, ha⟩) y z