awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
inr :
  ∀ (a : (↑Γ(Y, ⊤) : Type u)) (ha : Y.basicOpen a = (↑s : Y.Opens)),
    ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a
⊢ ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a

Tactic:
obtain ⟨a, ha⟩ := hUs s.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq_1 : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
hf' : P f'
e : (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) ≅ (↑(↑s : Y.Opens) : Scheme) :=
  IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ (↑s : Y.Opens)).ι ≫ U.ι) (↑s : Y.Opens).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
a : (↑Γ(Y, ⊤) : Type u)
ha : Y.basicOpen a = (↑s : Y.Opens)
w : (↑Γ(Y, ⊤) : Type u)
h : (↑s : Y.Opens) = Y.basicOpen a
⊢ ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a

Tactic:
use a, ha.symm

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr : Eq.{u + 1} (α := (↑U : Scheme).Opens) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)) ⊤
⊢ iSup V = ⊤

Tactic:
apply f.iSup_preimage_eq_top

Premises used: AlgebraicGeometry.Scheme.Hom.iSup_preimage_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr :
  Eq.{u + 1} (α := Y.Opens)
    ((fun (x : (↑U : Scheme).Opens) ↦ U.ι ''ᵁ x) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)))
    ((fun (x : (↑U : Scheme).Opens) ↦ U.ι ''ᵁ x) ⊤)
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)) ⊤

Tactic:
apply U.ι.image_injective

Premises used: AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.image_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr : ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = U.ι ''ᵁ ⊤
⊢ Eq.{u + 1} (α := Y.Opens)
    ((fun (x : (↑U : Scheme).Opens) ↦ U.ι ''ᵁ x) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)))
    ((fun (x : (↑U : Scheme).Opens) ↦ U.ι ''ᵁ x) ⊤)

Tactic:
simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Opens.opensRange_ι, AlgebraicGeometry.Scheme.Hom.image_iSup, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
rw : sSup Us
| U.ι ''ᵁ ⊤

Tactic:
rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι, heq]

Premises used: AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr : ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = sSup Us
⊢ ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = U.ι ''ᵁ ⊤

Tactic:
conv_rhs => rw [Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι, heq]

Premises used: AlgebraicGeometry.Scheme.Hom.image_top_eq_opensRange, AlgebraicGeometry.Scheme.Opens.opensRange_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
inr : (↑(⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens)) : Set ↥Y) = (↑(sSup Us) : Set ↥Y)
⊢ ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = sSup Us

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
i : (↑Us : Type u)
⊢ U ⊓ (↑i : Y.Opens) = (↑i : Y.Opens)

Tactic:
simp [heq, le_sSup i.property]

Premises used: le_sSup, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ ∀ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = (↑i : Y.Opens)

Tactic:
have (i : Us) : U ⊓ i.1 = i.1 := by simp [heq, le_sSup i.property]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
this_1 :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens} (f : X ⟶ (↑U : Scheme)) (hf : P f)
    (hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a), P (f ≫ U.ι)
hYa : ¬∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen
heq : U = sSup Us
V : (s : (↑Us : Type u)) → X.Opens := fun (s : (↑Us : Type u)) ↦ f ⁻¹ᵁ U.ι ⁻¹ᵁ (↑s : Y.Opens)
this : ∀ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = (↑i : Y.Opens)
⊢ (↑(⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens)) : Set ↥Y) = (↑(sSup Us) : Set ↥Y)

Tactic:
simp [this]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
U : Y.Opens
f : X ⟶ (↑U : Scheme)
hf : P f
hYa : ∃ (a : (↑Γ(Y, ⊤) : Type u)), U = Y.basicOpen a
obtain : ∀ (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f), P (f ≫ (Y.basicOpen a).ι)
⊢ P (f ≫ U.ι)

Tactic:
obtain ⟨a, rfl⟩ := hYa

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
        (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι))
    (hX : ¬IsAffine X), P (f ≫ (Y.basicOpen a).ι)
wlog :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
⊢ P (f ≫ (Y.basicOpen a).ι)

Tactic:
wlog hX : IsAffine X generalizing X Y

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f ≫ (Y.basicOpen a).ι)
⊢ P (f ≫ (Y.basicOpen a).ι)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : (↑X.affineOpens : Type u)
inr : P (((↑V : X.Opens).ι ≫ f) ≫ (Y.basicOpen a).ι)
⊢ P ((↑V : X.Opens).ι ≫ f ≫ (Y.basicOpen a).ι)

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : (↑X.affineOpens : Type u)
⊢ P (((↑V : X.Opens).ι ≫ f) ≫ (Y.basicOpen a).ι)

Tactic:
this _ _ (IsZariskiLocalAtSource.comp hf _) V.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
this :
  ∀ {X Y : Scheme.{u}} [IsAffine Y] (a : (↑Γ(Y, ⊤) : Type u)) (f : X ⟶ (↑(Y.basicOpen a) : Scheme)) (hf : P f)
    (hX : IsAffine X), P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : (↑X.affineOpens : Type u)
⊢ P (((↑V : X.Opens).ι ≫ f) ≫ (Y.basicOpen a).ι)

Tactic:
exact this _ _ (IsZariskiLocalAtSource.comp hf _) V.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : P f
hX : IsAffine X
rw :
  ∀ (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))) (hX : IsAffine X),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))
⊢ P (f ≫ (Y.basicOpen a).ι)

Tactic:
rw [HasRingHomProperty.iff_of_isAffine (P := P)] at hf ⊢

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))

Tactic:
hQ _ a _ hf

Premises used: Set.Mem, Set.univ, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst_1 : IsAffine Y
a : (↑Γ(Y, ⊤) : Type u)
f : X ⟶ (↑(Y.basicOpen a) : Scheme)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))

Tactic:
exact hQ _ a _ hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
inr :
  ∀
    (this :
      ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i))
    (hZ : ¬IsAffine Z), P (f ≫ i)
wlog : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
⊢ P (f ≫ i)

Tactic:
wlog hZ : IsAffine Z generalizing X Y Z

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
inr :
  ∀ (i_1 : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ i) ⁻¹ᵁ (↑i_1 : Z.Opens)) : Scheme)) ((f ≫ i) ∣_ (↑i_1 : Z.Opens))
⊢ P (f ≫ i)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
inr : P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ i ⁻¹ᵁ (↑U : Z.Opens) ≫ i ∣_ (↑U : Z.Opens))
⊢ P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ i) ∣_ (↑U : Z.Opens))

Tactic:
rw [morphismRestrict_comp]

Premises used: AlgebraicGeometry.morphismRestrict_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ i ⁻¹ᵁ (↑U : Z.Opens) ≫ i ∣_ (↑U : Z.Opens))

Tactic:
this _ inferInstance _ (IsZariskiLocalAtTarget.restrict hf _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Set.Mem, setOf, inferInstance, Set.preimage, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme.{u}} (i : Y ⟶ Z) (hi : IsOpenImmersion i) (f : X ⟶ Y) (hf : P f) (hZ : IsAffine Z), P (f ≫ i)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ i) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ i ⁻¹ᵁ (↑U : Z.Opens) ≫ i ∣_ (↑U : Z.Opens))

Tactic:
exact this _ inferInstance _ (IsZariskiLocalAtTarget.restrict hf _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, inferInstance, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
⊢ Eq (α := Set ↥Z) (Set.range (ι := ↥Y) ⇑i)
    (Set.range (ι := ↥(↑(Scheme.Hom.opensRange i) : Scheme)) ⇑(Scheme.Hom.opensRange i).ι)

Tactic:
simp