mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ : Scheme
⊢ ∀ {Z : Scheme} (e : Y✝ ≅ Z) (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e.hom)

Tactic:
_

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
⊢ ∀ (e : Y✝ ≅ Z✝) (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
⊢ ∀ (e : Y✝ ≅ Z✝) (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e.hom)

Tactic:
_

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
⊢ ∀ (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e✝.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
⊢ ∀ (f : X✝ ⟶ Y✝) [inst : IsAffine Y✝], of P f → of P (f ≫ e✝.hom)

Tactic:
_

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
⊢ ∀ [inst : IsAffine Y✝], of P f✝ → of P (f✝ ≫ e✝.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case h₂
P : MorphismProperty Scheme
inst✝ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
⊢ ∀ [inst : IsAffine Y✝], of P f✝ → of P (f✝ ≫ e✝.hom)

Tactic:
_

Goal state after:
case h₂
P : MorphismProperty Scheme
inst✝¹ : P.RespectsIso
X✝ Y✝ Z✝ : Scheme
e✝ : Y✝ ≅ Z✝
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ of P f✝ → of P (f✝ ≫ e✝.hom)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z : Scheme
⊢ ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'

Tactic:
X

Goal state after:
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X : Scheme
⊢ ∀ ⦃Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
⊢ ∀ [inst : IsAffine S] [inst_1 : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X},
    IsPullback g' f' f g → P g → P g'

Tactic:
_

Goal state after:
P : AffineTargetMorphismProperty
inst✝¹ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : AffineTargetMorphismProperty
inst✝¹ : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝ : IsAffine S
⊢ ∀ [inst : IsAffine X] {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'

Tactic:
_

Goal state after:
P : AffineTargetMorphismProperty
inst✝² : P.toProperty.RespectsIso
H : ∀ ⦃X Y S : Scheme⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (pullback.fst f g)
Z X Y S : Scheme
inst✝¹ : IsAffine S
inst✝ : IsAffine X
⊢ ∀ {f : X ⟶ S} {g : Y ⟶ S} {f' : Z ⟶ Y} {g' : Z ⟶ X}, IsPullback g' f' f g → P g → P g'
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
e₁ : m ≫ (D.vPullbackCone i j).fst = s.fst
⊢ m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
_

Goal state after:
case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
e₁ : m ≫ (D.vPullbackCone i j).fst = s.fst
a✝ : m ≫ (D.vPullbackCone i j).snd = s.snd
⊢ m = lift (D.f i j) s.fst ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
𝒰' : (i : 𝒰.I₀) → (pullback f (𝒰.f i)).OpenCover
inst✝ : ∀ (i : 𝒰.I₀) (j : (𝒰' i).I₀), IsAffine ((𝒰' i).X j)
h𝒰' : ∀ (i : 𝒰.I₀) (j k : (𝒰' i).I₀), Q (pullback.mapDesc ((𝒰' i).f j) ((𝒰' i).f k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover (pullback f f) :=
  Precoverage.ZeroHypercover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i ↦
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒱.I₀
⊢ IsAffine (𝒱.X i)

Tactic:
dsimp [𝒱]; infer_instance

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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
⊢ ∀ [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous f → (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
_

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ [inst : TopologicalSpace β] (f : α → β) {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst✝, _] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ [inst : TopologicalSpace β] (f : α → β) {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst✝, _] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
_

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
⊢ ∀ (f : α → β) {ι : Type u_1} (U : ι → Opens β),
    IsOpenCover U →
      Continuous[inst✝¹, inst✝] f →
        (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
⊢ Continuous[inst✝¹, inst✝] f →
    (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f

Tactic:
_

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
g : Y ⟶ Z
this : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ Function.Surjective).RespectsIso
α β : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
H : IsOpenCover U
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ (i : ι), Function.Surjective ((U i).carrier.restrictPreimage f)) → Function.Surjective f
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) * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1

Tactic:
IsLocalization.Away.sec_spec a x,

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⟩
⊢ (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1 * (algebraMap R (Rₜ ⟨a, ha⟩)) (a ^ 1) =
    (algebraMap R (Rₜ ⟨a, ha⟩)) a * (algebraMap R (Rₜ ⟨a, ha⟩)) (sec a x).1
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
⊢ IsDominant g

Tactic:
by
  rw [isDominant_iff, denseRange_iff_closure_range, ← Set.univ_subset_iff] at H ⊢
  exact H.trans (closure_mono (Set.range_comp_subset_range f g))

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: M S T : Scheme
inst✝¹ : M.Over S
f : T ⟶ S
inst✝ : MonObj (M.asOver S)
⊢ IsMonHom (Hom.asOver (pullback.fst (M ↘ S) (𝟙 S)) S)

Tactic:
unfold asOver OverClass.asOver at *; exact Over.isMonHom_pullbackFst_id_right

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
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S : Type u
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
_

Goal state after:
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),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: 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),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
_

Goal state after:
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),
    Ideal.span s = ⊤ →
      (∀ (r : ↑s),
          (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P)
            ((algebraMap S (Localization.Away ↑r)).comp f)) →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R✝ : Type u_1
⊢ ∀ {S : Type u_1} [inst : CommRing R✝] [inst_1 : CommRing S] (e : R✝ ≃+* S), Function.Surjective ⇑e.toRingHom

Tactic:
_

Goal state after:
R✝ S✝ : Type u_1
⊢ ∀ [inst : CommRing R✝] [inst_1 : CommRing S✝] (e : R✝ ≃+* S✝), Function.Surjective ⇑e.toRingHom
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R✝ S✝ : Type u_1
⊢ ∀ [inst : CommRing R✝] [inst_1 : CommRing S✝] (e : R✝ ≃+* S✝), Function.Surjective ⇑e.toRingHom

Tactic:
_

Goal state after:
R✝ S✝ : Type u_1
inst✝ : CommRing R✝
⊢ ∀ [inst : CommRing S✝] (e : R✝ ≃+* S✝), Function.Surjective ⇑e.toRingHom
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: R✝ S✝ : Type u_1
inst✝ : CommRing R✝
⊢ ∀ [inst : CommRing S✝] (e : R✝ ≃+* S✝), Function.Surjective ⇑e.toRingHom

Tactic:
_

Goal state after:
R✝ S✝ : Type u_1
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
⊢ ∀ (e : R✝ ≃+* S✝), Function.Surjective ⇑e.toRingHom
Module: Mathlib.RingTheory.RingHom.Surjective

Goal state before:
pp: case tmul
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Function.Surjective ⇑(algebraMap R T)
x : S
y : T
⊢ ∃ a, (algebraMap S (S ⊗[R] T)) a = x ⊗ₜ[R] y

Tactic:
| tmul x y =>

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_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
_

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝ : CommRing R
⊢ ∀ [inst : CommRing S] [inst_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)
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_1 : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
_

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ [inst : CommRing T] (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)
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),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)

Tactic:
_

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
⊢ ∀ (f : R →+* S) (g : S →+* T),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) g →
        (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) (g.comp f)
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:
dsimp [𝒱]; infer_instance

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_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra S T] (s : S)
    [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
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_1 : CommRing T] [inst_2 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)
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_1 : CommRing T] [inst_2 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
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_1 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)
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_1 : Algebra S T] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
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] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)
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] (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)

Tactic:
_

Goal state after:
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
⊢ ∀ (s : S) [IsLocalization.Away s T] (f : R →+* S),
    (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) f →
      (fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap S T).comp f)