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
x : ↑(PrimeSpectrum.Top R)
⊢ ModuleCat.Hom.hom (toStalkₗ' R M x) =
    ↑(stalkIsoₗ R M x).toLinearEquiv.symm ∘ₗ LocalizedModule.mkLinearMap x.asIdeal.primeCompl M

Tactic:
ext m

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
x : ↑(PrimeSpectrum.Top R)
m : ↑(ModuleCat.of R M)
⊢ (ModuleCat.Hom.hom (toStalkₗ' R M x)) m =
    (↑(stalkIsoₗ R M x).toLinearEquiv.symm ∘ₗ LocalizedModule.mkLinearMap x.asIdeal.primeCompl M) m
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ toStalkₗ R M x = ↑(modulePresheafStalkIso R M x).symm ∘ₗ ModuleCat.Hom.hom (toStalkₗ' R M x)

Tactic:
ext m

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
x : ↑(PrimeSpectrum.Top R)
m : M
⊢ (toStalkₗ R M x) m = (↑(modulePresheafStalkIso R M x).symm ∘ₗ ModuleCat.Hom.hom (toStalkₗ' R M x)) m
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
⊢ ⇑(Localizations.comapFun f.toSemilinearMap ↑p) =
    ⇑(Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯)

Tactic:
ext m

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥V
m : Localizations R (PrimeSpectrum.comap f ↑p)
⊢ (Localizations.comapFun f.toSemilinearMap ↑p) m =
    (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) m
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
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
rwa [PrimeSpectrum.comap_id]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) x =
    (ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y

Tactic:
dsimp only [coequalizer.π] at h

Goal state after:
D : GlueData
x y : ↑(∐ D.U)
h :
  (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) x =
    (ConcreteCategory.hom (colimit.ι (parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap) one)) y
diagram : WalkingParallelPair ⥤ Type u := parallelPair D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙ forget TopCat
⊢ (ConcreteCategory.hom (colimit.ι diagram one)) x = (ConcreteCategory.hom (colimit.ι diagram one)) y
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom x))

Tactic:
rcases (TopCat.epi_iff_surjective
    (coequalizer.π f.toShHom g.toShHom).hom.base).mp inferInstance x with ⟨y, rfl⟩

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
y : ↑↑Y.toPresheafedSpace
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom
        ((ConcreteCategory.hom (coequalizer.π (Hom.toShHom f) (Hom.toShHom g)).hom.base) y)))
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
i j k : 𝒰.I₀
⊢ t' 𝒰 f g i j k ≫
      pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i) ≫
        pullback.fst (pullback.fst (𝒰.f j ≫ f) g ≫ 𝒰.f j) (𝒰.f i) ≫ pullback.snd (𝒰.f j ≫ f) g =
    pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.f i ≫ f) g ≫ 𝒰.f i) (𝒰.f j) ≫ pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp only [t', Category.assoc, pullbackSymmetry_hom_comp_snd_assoc,
    pullbackRightPullbackFstIso_inv_fst_assoc, pullback.lift_fst_assoc, t_fst_snd,
    pullbackRightPullbackFstIso_hom_fst_assoc]

Goal state after:
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
⊢ (gluing 𝒰 f g).glued ⟶ Y

Tactic:
by
  apply Multicoequalizer.desc _ _ fun i ↦ pullback.snd _ _
  simp [t_fst_snd]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
⊢ IsIso (Sigma.desc f)

Tactic:
apply isIso_of_isOpenImmersion_of_opensRange_eq_top

Goal state after:
σ : Type v
inst✝¹ : Small.{u, v} σ
X : σ → Scheme
S : Scheme
f : (i : σ) → X i ⟶ S
inst✝ : ∀ (i : σ), IsOpenImmersion (f i)
hcov : ⨆ i, Scheme.Hom.opensRange (f i) = ⊤
hdisj : _root_.Pairwise (Disjoint on fun x ↦ Scheme.Hom.opensRange (f x))
this : IsOpenImmersion (Sigma.desc f)
⊢ Scheme.Hom.opensRange (Sigma.desc 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
⊢ gluedLift 𝒰 f g s ≫ p1 𝒰 f g = s.fst

Tactic:
by
  rw [← cancel_epi (Cover.fromGlued <| 𝒰.pullback₁ s.fst)]
  apply Multicoequalizer.hom_ext
  intro b
  simp_rw [Cover.fromGlued, Multicoequalizer.π_desc_assoc, gluedLift, ← Category.assoc]
  simp_rw [Cover.ι_glueMorphisms (𝒰.pullback₁ s.fst)]
  simp [p1, pullback.condition]

Goal state after:
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
R : ι → CommRingCat
⊢ IsOpenImmersion (sigmaSpec R)

Tactic:
by
  classical
  apply isOpenImmersion_sigmaDesc
  intro ix iy h
  refine Set.disjoint_iff_forall_ne.mpr ?_
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ e
  have : DFinsupp.single (β := (R ·)) iy 1 iy ∈ y.asIdeal :=
    (PrimeSpectrum.ext_iff.mp e).le (x := DFinsupp.single iy 1)
      (show DFinsupp.single (β := (R ·)) iy 1 ix ∈ x.asIdeal by simp [h.symm])
  simp [← Ideal.eq_top_iff_one, y.2.ne_top] at this

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
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)) ≫ (pullbackP1Iso 𝒰 f g i).hom) ≫ pullback.snd (𝒰.f i ≫ f) g =
    ((((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 ⋯ ⋯) ≫
      pullback.snd (𝒰.f i ≫ f) g

Tactic:
simp_rw [Category.assoc, pullbackP1Iso_hom_snd, pullback.lift_snd,
      pullbackSymmetry_hom_comp_snd_assoc, pullback.lift_fst_assoc, Category.comp_id,
      pullbackRightPullbackFstIso_hom_fst_assoc, ← pullback.condition_assoc, h₂]

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

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P f
i : 𝒰.I₀
⊢ P (𝒰.f i ≫ f)

pp: case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f

Tactic:
· rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
      P.cancel_left_of_respectsIso]
    exact restrict _ _ hf

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
restrict : ∀ {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)
of_sSup_eq_top :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P (𝒰.f i ≫ f)
⊢ P f
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x : ↑↑(D.U i)
⊢ (∃ x_1 ∈ U,
      (ConcreteCategory.hom (D.ι i).base) x_1 =
        (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x) →
    x ∈ U

Tactic:
rintro ⟨y, h1, h2⟩

Goal state after:
case w
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
x y : ↑↑(D.U i)
h1 : y ∈ U
h2 :
  (ConcreteCategory.hom (D.ι i).base) y =
    (ConcreteCategory.hom (colimit.ι D.diagram.multispan (WalkingMultispan.right i)).base) x
⊢ x ∈ U
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case restrict
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)

pp: case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f

Tactic:
· rw [eq_targetAffineLocally P]
    intro X Y f U H V
    rw [Q.arrow_mk_iso_iff (morphismRestrictRestrict f _ _)]
    exact H ⟨_, V.2.image_of_isOpenImmersion (Y.ofRestrict _)⟩

Goal state after:
case of_sSup_eq_top
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := ⋯
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
⊢ P (pullback.fst f g)

Tactic:
rw [P.iff_of_zeroHypercover_target (S.affineCover.pullback₁ f)]

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
hP' : Q.IsStableUnderBaseChange
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
H : P g
⊢ ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f S.affineCover).I₀),
    P (pullback.snd (pullback.fst f g) ((Precoverage.ZeroHypercover.pullback₁ f S.affineCover).f i))
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: case h
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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ (colimit.ι F ↓i) xi = x

Tactic:
apply ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv.isOpenEmbedding.injective

Goal state after:
case h
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
x : ↥(Limits.colimit F)
i : (glueData F).J
xi : ↥((glueData F).U i)
h : ((glueData F).ι i) xi = ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
⊢ ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv ((colimit.ι F ↓i) xi) =
    ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv x
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
x✝ : (a : ↑s) × ↑(t a)
a : ↑s
b : ↑(t a)
⊢ IsLocalization.Away (IsLocalization.Away.mulNumerator s t ⟨a, b⟩)
    ((fun x ↦
        match x with
        | ⟨a, b⟩ => Localization.Away ↑b)
      ⟨a, b⟩)

pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
⊢ ∀ (i : (a : ↑s) × ↑(t a)),
    P
      ((algebraMap S
            ((fun x ↦
                match x with
                | ⟨a, b⟩ => Localization.Away ↑b)
              i)).comp
        f)

Tactic:
· have : IsLocalization.Away ((algebraMap S (Localization.Away a.val))
        (IsLocalization.Away.sec a.val b.val).1) (Localization.Away b.val) := by
      apply IsLocalization.Away.of_associated (r := b.val)
      rw [← IsLocalization.Away.sec_spec]
      apply associated_mul_unit_right
      rw [map_pow _ _]
      exact IsUnit.pow _ (IsLocalization.Away.algebraMap_isUnit _)
    apply IsLocalization.Away.mul' (Localization.Away a.val) (Localization.Away b.val)

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set S
hsone : Ideal.span s = ⊤
t : (r : ↑s) → Set (Localization.Away ↑r)
htone : ∀ (r : ↑s), Ideal.span (t r) = ⊤
ht :
  ∀ (r : ↑s),
    ∀ t_1 ∈ t r,
      (fun {R S} [CommRing R] [CommRing S] ↦ P)
        ((algebraMap (Localization.Away ↑r) (Localization.Away t_1)).comp
          ((algebraMap S (Localization.Away ↑r)).comp f))
⊢ ∀ (i : (a : ↑s) × ↑(t a)),
    P
      ((algebraMap S
            ((fun x ↦
                match x with
                | ⟨a, b⟩ => Localization.Away ↑b)
              i)).comp
        f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
⊢ ∀ {T : Scheme} (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)], P (pullback.fst f_1 (𝒰.f i ≫ f))

Tactic:
intro T

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : P.universally f
i : 𝒰.I₀
T : Scheme
⊢ ∀ (f_1 : T ⟶ Y) [inst : HasPullback f_1 (𝒰.f i ≫ f)], P (pullback.fst f_1 (𝒰.f i ≫ f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
⊢ ∀ {T : Scheme} (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (pullback.fst f_1 f)

Tactic:
intro T

Goal state after:
case refine_2
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
𝒰 : Scheme.zariskiPrecoverage.ZeroHypercover X
hf : ∀ (i : 𝒰.I₀), P.universally (𝒰.f i ≫ f)
T : Scheme
⊢ ∀ (f_1 : T ⟶ Y) [inst : HasPullback f_1 f], P (pullback.fst f_1 f)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ P) (f ∣_ U) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))

Tactic:
dsimp only [sourceAffineLocally]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
⊢ (∀ (U_1 : ↑(↑(f ⁻¹ᵁ U)).affineOpens), P (CommRingCat.Hom.hom (Hom.appLE (f ∣_ U) ⊤ ↑U_1 ⋯))) ↔
    ∀ (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ U), P (CommRingCat.Hom.hom (Hom.appLE f U (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case hb
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis (Set.range fun U ↦ ↑U)

pp: case hb'
X : Scheme
U : Set ↥X
⊢ ∀ (i : ↑X.affineOpens), IsCompact ↑↑i

Tactic:
· rw [Subtype.range_coe]; exact X.isBasis_affineOpens

Goal state after:
case hb'
X : Scheme
U : Set ↥X
⊢ ∀ (i : ↑X.affineOpens), IsCompact ↑↑i
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ ↑↑V)

Tactic:
apply hV.union

Goal state after:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier → ∀ (U : ↑X.affineOpens), IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑U).carrier ∩ ↑↑V)

Tactic:
· intro S _ W hW
        change IsCompact ((S.1 ∪ W.1) ∩ V.1)
        rw [Set.union_inter_distrib_right]
        apply hW.union
        apply H

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

Goal state before:
pp: ⊢ OfLocalizationMaximal fun R x ↦ IsReduced R

Tactic:
introv R h

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ IsReduced R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
this : q.IsPrime
⊢ 1 ≤ q.height

Tactic:
Order.one_le_iff_ne_zero,

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
this : q.IsPrime
⊢ q.height ≠ 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I = IsLocalRing.maximalIdeal R → ↑I.height = ringKrullDim R

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
inst✝ : (IsLocalRing.maximalIdeal R).IsPrime
⊢ ↑(IsLocalRing.maximalIdeal R).height = ringKrullDim R
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := ⋯
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ Submodule.spanRank J + Submodule.spanRank (span {x}) ≤ ↑(r + 1)

Tactic:
push_cast

Goal state after:
case succ.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
r : ℕ
ih : ↑r ≤ I.height → ∃ J ≤ I, Submodule.spanRank J ≤ ↑r ∧ ↑r ≤ J.height
hr : ↑(r + 1) ≤ I.height
J : Ideal R
h₁ : J ≤ I
h₂ : Submodule.spanRank J ≤ ↑r
h₃ : ↑r ≤ J.height
S : Set (Ideal R) := {K | K ∈ J.minimalPrimes ∧ K.height = ↑r}
hS : S.Finite
x : R
hx₁ : x ∈ ↑I
hx₂ : ∀ x_1 ∈ S, x ∉ ↑x_1
⊢ Submodule.spanRank J + Submodule.spanRank (span {x}) ≤ ↑r + 1
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝² : HasRingHomProperty P Q
hP : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : (sourceAffineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q).IsLocal :=
  HasAffineProperty.isLocal_affineProperty P
X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme⦄ (g : Y ⟶ S), P g → IsAffine Y → P (pullback.fst f g)
hX : ¬IsAffine Y
⊢ P (pullback.fst f g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
      (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
    intro i
    simp only [Scheme.Pullback.openCoverOfRight_f, limit.lift_π, PullbackCone.mk_π_app,
      Category.comp_id]
    apply this _ (comp_of_isOpenImmersion _ _ _ H) inferInstance

Goal state after: