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

Goal state before:
pp: case mpr.refine_2
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1

Tactic:
← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst

Goal state after:
case mpr.refine_2
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.obj.obj (op U)) ↑(F.obj.obj (op V))))))
y : ↑(F.obj.obj (op W))
e₁ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.obj.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : U ≤ V
⊢ (isoImage f U).hom ≫ Y.homOfLE ⋯ = X.homOfLE e ≫ (isoImage f V).hom

Tactic:
by
  simp [← cancel_mono (f ''ᵁ V).ι]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f ≫ Y.toSpecΓ ≫ (asIso Y.toSpecΓ).inv = f

Tactic:
asIso_inv,

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

Goal state before:
pp: X : Scheme
⊢ ↑(⨆ i, ↑i) = ↑⊤

Tactic:
Opens.coe_iSup

Goal state after:
X : Scheme
⊢ ⋃ i, ↑↑i = ↑⊤
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: case refine_1
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))) → coequalizer f g ⟶ s.pt

pp: case refine_2
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))), coequalizer.π f g ≫ ?refine_1 s = s.inl

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) ≫ ?refine_1 s = 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 = ?refine_1 s

Tactic:
· refine fun s ↦ coequalizer.desc s.inl ?_
    have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
    have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
    exact H₁.trans H₂.symm

Goal state after:
case refine_2
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))),
    coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

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

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:
rw [toStalk_smul]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ (Localization.localRingHom (Ideal.comap f (↑x✝).asIdeal) (↑x✝).asIdeal f ⋯) (↑1 ⟨PrimeSpectrum.comap f ↑x✝, ⋯⟩) =
    ↑1 x✝

Tactic:
exact (Localization.localRingHom ..).map_one

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.fst i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).fst i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)
    ((ConcreteCategory.hom
        ((Cofan.mk (colimit.cocone (Discrete.functor D.diagram.right)).pt fun i ↦
                  D.diagram.snd i ≫
                    Cofan.inj (colimit.cocone (Discrete.functor D.diagram.right))
                      ((MultispanShape.prod D.J).snd i)).ι.app
            { as := (i, j) } ≫
          (sigmaIsoSigma D.U).hom))
      y)

Tactic:
erw [sigmaIsoSigma_hom_ι_apply, sigmaIsoSigma_hom_ι_apply]

Goal state after:
case mp
D : GlueData
i✝ j✝ : D.J
x : ↑(D.U i✝)
y✝ : ↑(D.U j✝)
h :
  (ConcreteCategory.hom (Sigma.ι D.diagram.right i✝ ≫ Multicoequalizer.sigmaπ D.diagram)) x =
    (ConcreteCategory.hom (Sigma.ι D.diagram.right j✝ ≫ Multicoequalizer.sigmaπ D.diagram)) y✝
i j : D.J
y : ↑(D.diagram.left (i, j))
⊢ D.Rel ⟨(MultispanShape.prod D.J).fst { as := (i, j) }.as, (D.diagram.fst { as := (i, j) }.as).hom' y⟩
    ⟨(MultispanShape.prod D.J).snd { as := (i, j) }.as, (D.diagram.snd { as := (i, j) }.as).hom' y⟩
Module: Mathlib.Topology.Gluing

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

Tactic:
by
  rw [← Set.preimage_image_eq (Set.range (D.f j i)) (D.ι_injective j), ← Set.image_univ, ←
    Set.image_univ, ← Set.image_comp, ← coe_comp, Set.image_univ, Set.image_univ, ← image_inter,
    Set.preimage_range_inter]

Goal state after:
Module: Mathlib.Topology.Gluing

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

Tactic:
rw [← this, Set.image_preimage_eq_inter_range]

Goal state after:
D : GlueData
i j : D.J
U : Set ↑(D.U i)
this :
  ⇑(ConcreteCategory.hom (D.f j i)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.t j i ≫ D.f i j)) ⁻¹' U
⊢ ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U =
    ⇑(ConcreteCategory.hom (D.ι j)) ⁻¹' ⇑(ConcreteCategory.hom (D.ι i)) '' U ∩
      Set.range ⇑(ConcreteCategory.hom (D.f j i))
Module: Mathlib.AlgebraicGeometry.Gluing

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

Tactic:
pullbackSymmetry_hom_comp_fst,

Goal state after:
case h.right
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : (𝒰.f i) x = (𝒰.f j) y
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j)))
      ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ (ConcreteCategory.hom (e.hom ≫ (pullback.snd (𝒰.f ⟨i, x⟩.fst) (𝒰.f ⟨j, y⟩.fst)).base)) ⟨(x, y), h⟩ = ⟨j, y⟩.snd
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t

Tactic:
rw [𝒰.gluedCover.isOpen_iff] at hU

Goal state after:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : x ∈ ⇑(fromGlued 𝒰) '' U
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
Module: Mathlib.AlgebraicGeometry.Limits

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

Tactic:
rw [IsOpenImmersion.iff_isIso_stalkMap]

Goal state after:
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ Topology.IsOpenEmbedding ⇑(Sigma.desc α) ∧ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)
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₀
⊢ pullback.snd (p1 𝒰 f g) (𝒰.f i) ≫ 𝒰.f i ≫ f = (pullback.fst (p1 𝒰 f g) (𝒰.f i) ≫ p2 𝒰 f g) ≫ g

Tactic:
rw [← pullback.condition_assoc, Category.assoc, p_comm]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this✝ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
this : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x))

Tactic:
have : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) :=
      IsOpenImmersion.of_isLocalization (0, 1)

Goal state after:
case inr
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
x : ↥(Spec (CommRingCat.of S))
this✝¹ :
  (((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x) =
    Scheme.Hom.stalkMap (coprodSpec R S) (coprod.inr x)
this✝ : Algebra (R × S) S := (RingHom.snd R S).toAlgebra
this : IsOpenImmersion (Spec.map (CommRingCat.ofHom (RingHom.snd R S)))
⊢ IsIso
    ((((Spec (CommRingCat.of (R × S))).presheaf.stalkCongr ⋯).hom ≫
        Scheme.Hom.stalkMap (Spec.map (CommRingCat.ofHom (RingHom.snd R S))) x) ≫
      inv (Scheme.Hom.stalkMap coprod.inr x))
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
⊢ IsIso (sigmaSpec R)

Tactic:
have : sigmaSpec R =
      (colimit.isoColimitCocone ⟨_,
        (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm _).symm (isColimitOfPreserves
          Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R)))⟩).hom := by
    ext1
    simp; rfl

Goal state after:
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S : Type u
inst✝² : CommRing R✝
inst✝¹ : CommRing S
inst✝ : Finite ι
R : ι → CommRingCat
this :
  sigmaSpec R =
    (colimit.isoColimitCocone
        {
          cocone :=
            (Cocone.precompose Discrete.natIsoFunctor.symm.hom).obj (Scheme.Spec.mapCocone (CommRingCat.piFan R).op),
          isColimit :=
            (IsColimit.precomposeHomEquiv Discrete.natIsoFunctor.symm
                  (Scheme.Spec.mapCocone (CommRingCat.piFan R).op)).symm
              (isColimitOfPreserves Scheme.Spec (Fan.IsLimit.op (CommRingCat.piFanIsLimit R))) }).hom
⊢ IsIso (sigmaSpec R)
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case left
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.left)))

pp: case right
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right)))

Tactic:
· simpa using! f.isOpenEmbedding.injective

Goal state after:
case right
U X Y : Scheme
f : U ⟶ X
g : U ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsOpenImmersion g
⊢ Function.Injective
    ⇑(ConcreteCategory.hom ((span f g ⋙ Scheme.forget).map (WidePushoutShape.Hom.init WalkingPair.right)))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case e_a.h₀
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.I₀), HasPullback (𝒰.f i ≫ f) g
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.snd (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.fst (𝒰.f i) s.fst

Tactic:
pullbackSymmetry_hom_comp_fst,

Goal state after:
case e_a.h₀
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.snd (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) ⋯ ⋯ ≫ pullback.snd s.fst (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case H
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ Set.range ⇑f ⊆ ↑(⨆ i, U i)

pp: case hf
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ ∀ (i : ↥X), P (f ∣_ U i)

Tactic:
· rintro y ⟨x, rfl⟩
    simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]
    exact ⟨x, h₁ x⟩

Goal state after:
case hf
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtTarget P
X Y : Scheme
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : P.HasOfPostcompProperty IsOpenImmersion
f : X ⟶ Y
U : ↥X → Y.Opens
h₁ : ∀ (x : ↥X), f x ∈ U x
h₂ : ∀ (x : ↥X), P ((f ⁻¹ᵁ U x).ι ≫ f)
⊢ ∀ (i : ↥X), P (f ∣_ U i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ P ((V x).ι ≫ f)

Tactic:
← Scheme.Hom.resLE_comp_ι _ (e x)

Goal state after:
P : MorphismProperty Scheme
inst✝² : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : P.RespectsRight IsOpenImmersion
U : ↥X → Y.Opens
V : ↥X → X.Opens
hxU : ∀ (x : ↥X), x ∈ (V x).carrier
e : ∀ (x : ↥X), V x ≤ f ⁻¹ᵁ U x
hf : ∀ (x : ↥X), P (Scheme.Hom.resLE f (U x) (V x) ⋯)
x : ↥X
⊢ P (Scheme.Hom.resLE f (U x) (V x) ⋯ ≫ (U 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
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
f : ↓i ⟶ ↓j
this : V F (↓i) ↓j = ⊤
⊢ IsIso (V F (↓i) ↓j).ι

Tactic:
exact this ▸ (topIso _).isIso_hom

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)
⊢ Mono
    ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))

Tactic:
apply +allowSynthFailures mono_comp

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)
⊢ Mono
    ((D.diagram.multispan.map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))).unop).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))
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)
⊢ Mono
    ((D.f j i).c.app
        (op
          ((Opens.map
                (colimit.ι D.diagram.multispan
                    (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
            (⋯.functor.obj U))) ≫
      (D.t i j).c.app
        (op
          ((Opens.map (D.f j i).base).obj
            (unop
              (op
                ((Opens.map
                      (colimit.ι D.diagram.multispan
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                  (⋯.functor.obj U)))))))

Tactic:
apply +allowSynthFailures mono_comp

Goal state after:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
H : ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.I₀), Q (𝒰.f i ≫ f)
⊢ IsZariskiLocalAtSource P

Tactic:
by
  refine .mk_of_small (fun {X Y f} 𝒰 hf ↦ ?_) (fun {X Y f} 𝒰 hf ↦ ?_) <;>
  simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y),
      HasAffineProperty.iff_of_isAffine, morphismRestrict_comp] at hf ⊢
  · intro i U
    let 𝒰' : X.OpenCover := (Scheme.Cover.ulift 𝒰).add (𝒰.f i)
    exact (H (f ∣_ U.1) (𝒰'.restrict _)).mp (hf _) none
  · intro U
    rw [H (f ∣_ U.1) (Scheme.OpenCover.restrict 𝒰 _)]
    intro i
    exact hf _ _

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Lemmas

Goal state before:
pp: case h
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 * (algebraMap R (Rₜ ⟨a, ha⟩)) a ^ ((sec a x).2 + 1) = (algebraMap R (Rₜ ⟨a, ha⟩)) (a * (sec a x).1)

Tactic:
map_mul,

Goal state after:
case h
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 * (algebraMap R (Rₜ ⟨a, ha⟩)) a ^ ((sec a x).2 + 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1