awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P.IsStableUnderBaseChange
have hP' : AffineTargetMorphismProperty.IsStableUnderBaseChange.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
Tactic: apply HasAffineProperty.isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u}
    (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
have hP' : ∀ ⦃X Y S : Scheme.{u}⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
  sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g →
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := pullback f g) (pullback.fst f g)
Tactic: apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
⊢ sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := pullback f g) (pullback.fst f g)
have hP' : ∀ (H : P g), P (X := pullback f g) (pullback.fst f g)
Tactic: rw [← HasAffineProperty.iff_of_isAffine (P := P)] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
⊢ P (X := pullback f g) (pullback.fst f g)
have hP' : ∀ (this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g))
  (hX : ¬IsAffine Y), P (X := pullback f g) (pullback.fst f g)
Tactic: wlog hX : IsAffine Y generalizing Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
hP' :
  ∀ (this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g))
    (hX : ¬IsAffine Y), P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback f g) (pullback.fst f g)
have wlog : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
Tactic: wlog hX : IsAffine Y generalizing Y
Cleared hypotheses: Y, g, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
hX : ¬IsAffine Y
⊢ P (X := pullback f g) (pullback.fst f g)
have hP' : ∀ (i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀),
  P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P)
      (Scheme.Pullback.openCoverOfRight Y.affineCover f g)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X Y S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
H : P g
this : ∀ ⦃Y : Scheme.{u}⦄ (g : Y ⟶ S) (H : P g) (hX : IsAffine Y), P (X := pullback f g) (pullback.fst f g)
hX : ¬IsAffine Y
i : (Scheme.Pullback.openCoverOfRight Y.affineCover f g).I₀
⊢ P ((Scheme.Pullback.openCoverOfRight Y.affineCover f g).f i ≫ pullback.fst f g)
have hP' : P (X := pullback f (Y.affineCover.f i ≫ g)) (pullback.fst f (Y.affineCover.f i ≫ g))
Tactic: simp only [Scheme.Pullback.openCoverOfRight_X, Scheme.Pullback.openCoverOfRight_f,
      limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : AffineTargetMorphismProperty.IsLocal.{u}
  (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) :=
  ⋯
X S : Scheme
inst_1 : IsAffine S
inst_2 : IsAffine X
f : X ⟶ S
Y : Scheme
g : Y ⟶ S
H : P g
hX : IsAffine Y
⊢ P (X := pullback f g) (pullback.fst f g)
have rw : ∀ (H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))) (hX : IsAffine Y),
  Q (S := (↑Γ(pullback f g, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (pullback.fst f g)))
Tactic: rw [iff_of_isAffine (P := P)] at H ⊢
Cleared hypotheses: H, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ P (f ≫ U.ι)
have inr : ∀
  (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), P (f ≫ U.ι)
Tactic: wlog hYa : ∃ (a : Γ(Y, ⊤)), U = Y.basicOpen a generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
inr :
  ∀
    (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), P (f ≫ U.ι)
⊢ P (f ≫ U.ι)
have wlog : ∀ {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.ι)
Tactic: wlog hYa : ∃ (a : Γ(Y, ⊤)), U = Y.basicOpen a generalizing X Y
Cleared hypotheses: X, Y, inst_1, U, f, hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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
⊢ P (f ≫ U.ι)
have inr : ∀ (Us : Set Y.Opens) (hUs : Us ⊆ Set.range (ι := (↑Γ(Y, ⊤) : Type u)) Y.basicOpen) (heq : U = sSup Us), P (f ≫ U.ι)
Tactic: obtain ⟨(Us : Set Y.Opens), hUs, heq⟩ := Opens.isBasis_iff_cover.mp (isBasis_basicOpen Y) U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ P (f ≫ U.ι)
have inr : ∀ (i : (↑Us : Type u)), P ((V i).ι ≫ f ≫ U.ι)
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) V]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)), P ((V i).ι ≫ f ≫ U.ι)
⊢ P (f ≫ U.ι)
have inr₁ : iSup V = ⊤
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) V]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
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)
s : (↑Us : Type u)
f' : (↑(V s) : Scheme) ⟶ (↑(U.ι ⁻¹ᵁ (↑s : Y.Opens)) : Scheme) := f ∣_ U.ι ⁻¹ᵁ (↑s : Y.Opens)
⊢ P ((V s).ι ≫ f ≫ U.ι)
have hf' : P f'
Tactic: have hf' : P f' := IsZariskiLocalAtTarget.restrict hf _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
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)
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).ι ⋯
⊢ P ((V s).ι ≫ f ≫ U.ι)
have heq₁ : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s : Y.Opens).ι
Tactic: have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
        simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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).ι
⊢ P ((V s).ι ≫ f ≫ U.ι)
have inr : P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)
Tactic: rw [heq, ← Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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).ι
⊢ P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)
have inr : P (f' ≫ e.hom)
Tactic: refine this _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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 : P (f' ≫ e.hom)
⊢ P ((f' ≫ e.hom) ≫ (↑s : Y.Opens).ι)
have inr₁ : ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a
Tactic: refine this _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)), (↑s : Y.Opens) = Y.basicOpen a
have inr : ∀ (a : (↑Γ(Y, ⊤) : Type u)) (ha : Y.basicOpen a = (↑s : Y.Opens)),
  ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a
Tactic: obtain ⟨a, ha⟩ := hUs s.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ ∃ (a : (↑Γ(Y, ⊤) : Type u)), (↑s : Y.Opens) = Y.basicOpen a
have h : (↑s : Y.Opens) = Y.basicOpen a
Tactic: use a, ha.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ iSup V = ⊤
have inr : Eq.{u + 1} (α := (↑U : Scheme).Opens) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)) ⊤
Tactic: apply f.iSup_preimage_eq_top
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens) (⨆ (i : (↑Us : Type u)), U.ι ⁻¹ᵁ (↑i : Y.Opens)) ⊤
have 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) ⊤)
Tactic: apply U.ι.image_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
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)
⊢ 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) ⊤)
have inr : ⨆ (i : (↑Us : Type u)), U ⊓ (↑i : Y.Opens) = U.ι ''ᵁ ⊤
Tactic: simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι]