awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
⊢ HasRingHomProperty.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
    fun {x S : Type u_1} {x_1 : CommRing x} {x_2 : CommRing S} (φ : x →+* S) ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)
have this : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
Tactic: have := stalkwiseIsZariskiLocalAtTarget_of_respectsIso hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
⊢ HasRingHomProperty.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
    fun {x S : Type u_1} {x_1 : CommRing x} {x_2 : CommRing S} (φ : x →+* S) ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)
have this₁ : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
Tactic: have := stalkwise_isZariskiLocalAtSource_of_respectsIso hP
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u_1} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso @P
this_1 : IsZariskiLocalAtTarget.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
this : IsZariskiLocalAtSource.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
⊢ HasRingHomProperty.{u_1} (AlgebraicGeometry.stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P)
    fun {x S : Type u_1} {x_1 : CommRing x} {x_2 : CommRing S} (φ : x →+* S) ↦
    ∀ (p : Ideal S) (x_3 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ ⋯)
have h : ∀ (R S : Type u_1) (x : CommRing R) (x_1 : CommRing S) (φ : R →+* S),
  (∀ (p : Ideal S) (x_2 : p.IsPrime),
      P (R := Localization.AtPrime (Ideal.comap φ p)) (S := Localization.AtPrime p)
        (Localization.localRingHom (Ideal.comap φ p) p φ sorry)) ↔
    AlgebraicGeometry.stalkwise (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ P) (Spec.map (CommRingCat.ofHom φ))
Tactic: convert!
    of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget (P := AlgebraicGeometry.stalkwise P) with R
    S _ _ φ
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
⊢ P (f ≫ g)
have inr : ∀ (this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
  (hZ : ¬IsAffine Z), P (f ≫ g)
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
inr :
  ∀ (this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
    (hZ : ¬IsAffine Z), P (f ≫ g)
⊢ P (f ≫ g)
have wlog : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
Cleared hypotheses: X, Y, Z, f, g, hf, hg
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
⊢ P (f ≫ g)
have inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ g) ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑i : Z.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))
have inr : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))
Tactic: rw [morphismRestrict_comp]
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
⊢ P (f ≫ g)
have inr : ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g))
  (hY : ¬IsAffine Y), P (f ≫ g)
Tactic: wlog hY : IsAffine Y 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g))
    (hY : ¬IsAffine Y), P (f ≫ g)
⊢ P (f ≫ g)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
Tactic: wlog hY : IsAffine Y generalizing X Y
Cleared hypotheses: X, Y, f, g, hf, hg
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
⊢ P (f ≫ g)
have inr : ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
  P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) (Y.affineCover.pullback₁ f)]
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hY : IsAffine Y), P (f ≫ g)
hY : ¬IsAffine Y
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ P ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i ≫ f ≫ g)
have inr : P (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i ≫ Y.affineCover.f i ≫ g :
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Z)
Tactic: rw [← Scheme.Cover.pullbackHom_map_assoc]
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
⊢ P (f ≫ g)
have inr : ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)) (hX : ¬IsAffine X), P (f ≫ g)
Tactic: wlog hX : IsAffine X generalizing X
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
inr : ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)) (hX : ¬IsAffine X), P (f ≫ g)
⊢ P (f ≫ g)
have wlog : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)
Tactic: wlog hX : IsAffine X generalizing X
Cleared hypotheses: X, 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)
hX : ¬IsAffine X
⊢ P (f ≫ g)
have inr : ∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f ≫ g)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover]
-- 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.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hY : IsAffine Y
this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hf : P f) (hX : IsAffine X), P (f ≫ g)
hX : ¬IsAffine X
i : X.affineCover.I₀
⊢ P (X.affineCover.f i ≫ f ≫ g)
have inr : P ((X.affineCover.f i ≫ f) ≫ g)
Tactic: rw [← 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hP : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Z : Scheme
hZ : IsAffine Z
Y : Scheme
g : Y ⟶ Z
hg : P g
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
hf : P f
hX : IsAffine X
⊢ P (f ≫ g)
have rw : ∀ (hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))) (hY : IsAffine Y) {X : Scheme.{u}} (f : X ⟶ Y)
  (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))) (hX : IsAffine X),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))
Tactic: rw [iff_of_isAffine (P := P)] at hf hg ⊢
Cleared hypotheses: hg, hY, X, f, hf, hX
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
⊢ P f
have inr : ∀ (this : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f) (hZ : ¬IsAffine Z), P f
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
inr :
  ∀ (this : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f) (hZ : ¬IsAffine Z),
    P f
⊢ P f
have wlog : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f
Tactic: wlog hZ : IsAffine Z generalizing X Y Z
Cleared hypotheses: X, Y, Z, f, 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f
hZ : ¬IsAffine Z
⊢ P f
have inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑i : Z.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _
      (g.iSup_preimage_eq_top (iSup_affineOpens_eq_top Z))]
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))
have inr : ∀ (H : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))),
  P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))
Tactic: have H := IsZariskiLocalAtTarget.restrict h U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H_1 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
this : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
H : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))
⊢ P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))
have H₁ : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))
Tactic: rw [morphismRestrict_comp] 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
⊢ P f
have inr : ∀ (this : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f) (hY : ¬IsAffine Y), P f
Tactic: wlog hY : IsAffine Y 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
inr :
  ∀ (this : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f) (hY : ¬IsAffine Y), P f
⊢ P f
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f
Tactic: wlog hY : IsAffine Y generalizing X Y
Cleared hypotheses: X, Y, f, 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f
hY : ¬IsAffine Y
⊢ P f
have inr : ∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top Y)]
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
have inr : ∀ (H : P ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f ≫ g)), P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
Tactic: have H := comp_of_isOpenImmersion P (f ⁻¹ᵁ U.1).ι (f ≫ g) h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H_1 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hZ : IsAffine Z
this : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
H : P ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f ≫ g)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
have H₁ : P (f ∣_ (↑U : Y.Opens) ≫ (↑U : Y.Opens).ι ≫ g)
Tactic: rw [← morphismRestrict_ι_assoc] 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY : IsAffine Y
⊢ P f
have inr : ∀ (this : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f) (hY : ¬IsAffine X), P f
Tactic: wlog hY : IsAffine X generalizing X
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY : IsAffine Y
inr : ∀ (this : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f) (hY : ¬IsAffine X), P f
⊢ P f
have wlog : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f
Tactic: wlog hY : IsAffine X generalizing X
Cleared hypotheses: X, f, h
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY_1 : IsAffine Y
this : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f
hY : ¬IsAffine X
⊢ P f
have inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f)
Tactic: rw [IsZariskiLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top X)]
-- 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
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY_1 : IsAffine Y
this : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f
hY : ¬IsAffine X
U : (↑X.affineOpens : Type u)
⊢ P ((↑U : X.Opens).ι ≫ f)
have inr : ∀ (H : P ((↑U : X.Opens).ι ≫ f ≫ g)), P ((↑U : X.Opens).ι ≫ f)
Tactic: have H := comp_of_isOpenImmersion P U.1.ι (f ≫ g) h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H_1 :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
X Y : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h : P (f ≫ g)
hY_1 : IsAffine Y
this : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f
hY : ¬IsAffine X
U : (↑X.affineOpens : Type u)
H : P ((↑U : X.Opens).ι ≫ f ≫ g)
⊢ P ((↑U : X.Opens).ι ≫ f)
have H₁ : P (((↑U : X.Opens).ι ≫ f) ≫ g)
Tactic: rw [← Category.assoc] 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_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
H :
  ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
    Q (g.comp f) → Q g
Z : Scheme
hZ : IsAffine Z
Y : Scheme
g : Y ⟶ Z
hY_1 : IsAffine Y
X : Scheme
f : X ⟶ Y
h : P (f ≫ g)
hY : IsAffine X
⊢ P f
have rw : ∀ (h : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))) (hY : IsAffine X),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Tactic: rw [iff_of_isAffine (P := P)] at h ⊢
Cleared hypotheses: h, hY