mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Submonoid.powers 1 ≤ IsUnit.submonoid S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ P ((algebraMap S (Localization.Away 1)).comp (algebraMap R S))

Tactic:
let e : S ≃ₐ[R] (Localization.Away (1 : S)) :=
    (IsLocalization.atUnits S (Submonoid.powers 1) (by simp)).restrictScalars R

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
this : Q.IsLocal := isLocal_affineProperty P
hf : Q.diagonal (pullback.snd f (𝟙 Y))
𝒰 : Scheme.Cover (Scheme.precoverage IsOpenImmersion) (pullback f (𝟙 Y)) :=
  Scheme.Cover.pushforwardIso X.affineCover (inv (pullback.fst f (𝟙 Y)))
i : 𝒰.I₀
⊢ IsAffine (𝒰.X i)

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝¹ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ Q.diagonal f ↔ P.diagonal f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i : 𝒱.I₀
⊢ IsAffine (𝒱.X i)

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ f) ≫ 𝟙 Y = 𝒰.f i.1 ≫ f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ f) ≫ 𝟙 Y = 𝒰.f i.2 ≫ f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y) = 𝟙 (𝒰.X i.1) ≫ 𝒰.f i.1

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y) = 𝟙 (𝒰.X i.2) ≫ 𝒰.f i.2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: ⊢ OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f ↦ Function.Surjective ⇑f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y) = 𝒰.f i.1 ≫ f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y) = 𝒰.f i.2 ≫ f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ (pullback.fst (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫
        (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y)) ≫
      (Iso.refl X).hom =
    (asIso
          (pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.1) (𝒰.f i.2)
            (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.fst f (𝟙 Y)) ⋯ ⋯)).hom ≫
      pullback.fst (𝒰.f i.1) (𝒰.f i.2) ≫ 𝒰.f i.1

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯)
        ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y)) (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.snd f (𝟙 Y))
        ⋯ ⋯ ≫
      (pullback.congrHom ⋯ ⋯).hom =
    (asIso
          (pullback.map (𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) (𝒰.f i.1) (𝒰.f i.2)
            (𝟙 (𝒰.X i.1)) (𝟙 (𝒰.X i.2)) (pullback.fst f (𝟙 Y)) ⋯ ⋯)).hom ≫
      pullback.mapDesc (𝒰.f i.1) (𝒰.f i.2) f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.diagonal f ≫ (Iso.refl (pullback.diagonalObj f)).hom = (Iso.refl X).hom ≫ pullback.diagonal f

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
𝒱 : (pullback f f).OpenCover := Scheme.Pullback.openCoverOfLeftRight 𝒰 𝒰 f f
i1 : ∀ (i : 𝒱.I₀), IsAffine (𝒱.X i)
i : 𝒱.toPreZeroHypercover.1
⊢ pullback.map ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.snd f (𝟙 Y)) f f
        ((𝒰.f i.1 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y))
        ((𝒰.f i.2 ≫ pullback.lift (𝟙 X) f ⋯) ≫ pullback.fst f (𝟙 Y)) (𝟙 Y) ⋯ ⋯ ≫
      (Iso.refl (pullback.diagonalObj f)).hom =
    (pullback.congrHom ⋯ ⋯).hom ≫ pullback.map (𝒰.f i.1 ≫ f) (𝒰.f i.2 ≫ f) f f (𝒰.f i.1) (𝒰.f i.2) (𝟙 Y) ⋯ ⋯

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝² : Q.IsLocal
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : IsAffine Y
h𝒰 : ∀ (i j : 𝒰.I₀), Q (pullback.mapDesc (𝒰.f i) (𝒰.f j) f)
⊢ Q.diagonal f

Tactic:
by

Goal state after:
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)
t : T
ht : t ∈ ↑sg
⊢ 1 ∈ Ideal.span (Set.range fun a ↦ ↑a)

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
𝒰 : Y.OpenCover := Y.openCoverOfIsOpenCover (fun f ↦ Y.basicOpen ↑f) ⋯
this : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
i : 𝒰.toPreZeroHypercover.1
⊢ Y.basicOpen ↑i = Scheme.Hom.opensRange (𝒰.f i)

Tactic:
by

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

Goal state before:
pp: Q : AffineTargetMorphismProperty
inst✝ : Q.IsLocal
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hs' : ∀ (r : ↥s), Q.diagonal (f ∣_ Y.basicOpen ↑r)
⊢ Q.diagonal f

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
⊢ P.diagonal = targetAffineLocally Q.diagonal

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
U : X.Opens
⊢ (U.ι ≫ f) ≫ 𝟙 Y = U.ι ≫ f

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource P.diagonal

Tactic:
by

Goal state after:
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)
⊢ (algebraMap T (Localization.Away a')).comp (g.comp f) =
    (Localization.awayMap g' ↑a).comp ((algebraMap S (Localization.Away ↑a)).comp f)

Tactic:
by

Goal state after:
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
⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPa : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

Goal state after:
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
hPb : IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
a : ↑s
⊢ IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
s : Set S
hsone : Ideal.span s = ⊤
hs : ∀ t ∈ s, (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S (Localization.Away t)).comp f)
rₐ : (a : ↑s) → Localization.Away ↑a := fun a ↦ (algebraMap S (Localization.Away ↑a)) (f r)
Sₐ : ↑s → Type u := fun a ↦ Localization.Away (rₐ a)
this✝ : ∀ (a : ↑s), IsLocalization.Away (((algebraMap S (Localization.Away ↑a)).comp f) r) (Sₐ a)
this :
  ∀ (a : ↑s),
    IsLocalization (Algebra.algebraMapSubmonoid (Localization.Away ↑a) (Submonoid.map f (Submonoid.powers r))) (Sₐ a)
a : ↑s
⊢ Submonoid.powers (f r) ≤ Submonoid.comap (algebraMap S (Localization.Away ↑a)) (Submonoid.powers (rₐ a))

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), IsOpenCover U → (∀ (i : ι), P (f ∣_ U i)) → P f
⊢ IsZariskiLocalAtTarget P.universally

Tactic:
by

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtSource P
⊢ IsZariskiLocalAtSource P.universally

Tactic:
by

Goal state after:
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
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P) (f ≫ g)

Tactic:
by

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f
⊢ MorphismProperty.isomorphisms Scheme ≤ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P

Tactic:
by

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
by

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ IsZariskiLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by

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

Goal state before:
pp: P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P).RespectsIso
hP₁ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ (U : Opens X), P f → P (f ∘ Subtype.val)
hP₂ :
  ∀ {X Y : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
    Continuous f → ∀ {ι : Type u} (U : ι → Opens X), IsOpenCover U → (∀ (i : ι), P (f ∘ Subtype.val)) → P f
⊢ IsZariskiLocalAtSource (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ P)

Tactic:
by

Goal state after: