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

Goal state before:
pp: case h₁
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (e.hom ≫ f))

pp: case h₂
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (f ≫ e.hom))

Tactic:
·

Goal state after:
case h₁
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : IsAffine Z],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ Y) (f₂ : U₂ ⟶ Y) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (e.hom ≫ f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case h₂
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (f ≫ e.hom))

Tactic:
·

Goal state after:
case h₂
P : AffineTargetMorphismProperty
inst✝ : P.toProperty.RespectsIso
⊢ ∀ {X Y Z : Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [inst : IsAffine Y],
    (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ f)) →
      ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
        [IsOpenImmersion f₂], P (pullback.mapDesc f₁ f₂ (f ≫ e.hom))
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},
    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},
    m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₁
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), SpecializingMap ⇑f

pp: case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)

Tactic:
·

Goal state after:
case hP₁
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), SpecializingMap ⇑f
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)

Tactic:
·

Goal state after:
case hP₂
⊢ ∀ {α β γ : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
    (f : α → β) (g : β → γ), SpecializingMap f → SpecializingMap g → SpecializingMap (g ∘ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₂
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)

pp: case hP₃
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)) → SpecializingMap f

Tactic:
·

Goal state after:
case hP₂
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → SpecializingMap f → SpecializingMap (s.restrictPreimage f)
Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

Goal state before:
pp: case hP₃
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)) → SpecializingMap f

Tactic:
·

Goal state after:
case hP₃
⊢ ∀ {α β : Type u_1} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u_1}
    (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), SpecializingMap ((U i).carrier.restrictPreimage f)) → SpecializingMap f
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))

pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Tactic:
·

Goal state after:
case h₀
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom includeLeftRingHom ≫ ofHom ↑(lmul' R))
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))

Tactic:
·

Goal state after:
case h₁
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Spec.map (𝟙 (of S)) = Spec.map (ofHom ↑includeRight ≫ ofHom ↑(lmul' R))
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
·

Goal state after:
case mp
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f →
    ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f

Tactic:
·

Goal state after:
case mpr
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ (∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)) →
    Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)

pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
·

Goal state after:
case refine_1
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝³ : ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs : ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
t : S
ht : t ∈ s
Sₜ : Type u
x✝² : CommRing Sₜ
x✝¹ : Algebra S Sₜ
x✝ : IsLocalization.Away t Sₜ
⊢ P ((algebraMap S Sₜ).comp f)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)

Tactic:
·

Goal state after:
case refine_2
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
hP : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
f : R →+* S
x✝ :
  ∃ s,
    ∃ (_ : Ideal.span ↑s = ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
          P ((algebraMap S Sₜ).comp f)
s : Finset S
hsone : Ideal.span ↑s = ⊤
hs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra S Sₜ] [IsLocalization.Away t Sₜ],
      P ((algebraMap S Sₜ).comp f)
⊢ ∃ s, ∃ (_ : Ideal.span ↑s = ⊤), ∀ t ∈ s, P ((algebraMap S (Localization.Away t)).comp f)
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:
·

Goal state after:
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⟩)
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
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:
·

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.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
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ Ideal.span (⇑e '' s) = ⊤

pp: case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))

Tactic:
·

Goal state after:
case refine_1
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ Ideal.span (⇑e '' s) = ⊤
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))

Tactic:
·

Goal state after:
case refine_2
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
R S T : Type u
x✝³ : CommRing R
x✝² : CommRing S
x✝¹ : CommRing T
f : R →+* S
e : S ≃+* T
x✝ : Locally (fun {R S} [CommRing R] [CommRing S] ↦ P) f
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)
⊢ ∀ t ∈ ⇑e '' s,
    (fun {R S} [CommRing R] [CommRing S] ↦ P) ((algebraMap T (Localization.Away t)).comp (e.toRingHom.comp f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case convert_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsAffine (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))

pp: case convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)

Tactic:
·

Goal state after:
case convert_1
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsAffine (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: case convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)

Tactic:
·

Goal state after:
case convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y U✝ V✝ : Scheme
f : X ⟶ Y
g : U✝ ⟶ Y
inst✝¹ : IsAffine U✝
inst✝ : IsOpenImmersion g
iV : V✝ ⟶ X
f' : V✝ ⟶ U✝
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
⊢ IsOpenImmersion
    (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g) g
      ⋯ ⋯)
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
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)
⊢ Ideal.span
      (Set.range fun x ↦
        match x with
        | (a, b) => g ↑a * ↑b) =
    ⊤

pp: case refine_2
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)
⊢ ∀ (i : ↥sf × ↥sg),
    P
      ((algebraMap T
            ((fun x ↦
                match x with
                | (a, b) => Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))
              i)).comp
        (g.comp f))

Tactic:
·

Goal state after:
case refine_1
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)
⊢ Ideal.span
      (Set.range fun x ↦
        match x with
        | (a, b) => g ↑a * ↑b) =
    ⊤