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_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
inr : ∀ (i : X.affineCover.I₀), P (X.affineCover.f i ≫ f ≫ g)
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- 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
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₀
inr : P ((X.affineCover.f i ≫ f) ≫ g)
⊢ P (X.affineCover.f i ≫ f ≫ g)

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_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)

Tactic:
this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance

Premises used: AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, inferInstance
-- 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
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)

Tactic:
exact this _ (comp_of_isOpenImmersion _ _ _ hf) inferInstance

Premises used: AlgebraicGeometry.HasRingHomProperty.comp_of_isOpenImmersion, inferInstance
-- 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
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
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)))
⊢ P (f ≫ g)

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

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_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 : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hY : IsAffine Y
X : Scheme
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:
hP _ _ hg 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_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 : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hY : IsAffine Y
X : Scheme
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:
exact hP _ _ hg 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
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
wlog : ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hZ : IsAffine Z), P f
⊢ P f

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
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
inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑i : Z.Opens))
⊢ P f

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

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.Scheme.Hom.iSup_preimage_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
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)
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))
⊢ P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))

Tactic:
have H := IsZariskiLocalAtTarget.restrict h U.1
-- 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
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) ≫ g ∣_ (↑U : Z.Opens))

Tactic:
rw [morphismRestrict_comp] at H

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
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) ≫ g ∣_ (↑U : Z.Opens))
⊢ P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))

Tactic:
this H inferInstance

Premises used: inferInstance
-- 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
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) ≫ g ∣_ (↑U : Z.Opens))
⊢ P (X := (↑(f ⁻¹ᵁ g ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens))

Tactic:
exact this H inferInstance

Premises used: inferInstance
-- 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
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
wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} {g : Y ⟶ Z} (h : P (f ≫ g)) (hY : IsAffine Y), P f
⊢ P f

Tactic:
wlog hY : IsAffine Y 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_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
inr : ∀ (i : (↑Y.affineOpens : Type u)), P (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
⊢ P f

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

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
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)
inr : ∀ (H : P ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ f ≫ g)), P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
have H := comp_of_isOpenImmersion P (f ⁻¹ᵁ U.1).ι (f ≫ g) h
-- 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
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 (f ∣_ (↑U : Y.Opens) ≫ (↑U : Y.Opens).ι ≫ g)

Tactic:
rw [← morphismRestrict_ι_assoc] at H

Premises used: AlgebraicGeometry.morphismRestrict_ι_assoc
-- 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
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) ≫ (↑U : Y.Opens).ι ≫ g)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
this H inferInstance

Premises used: inferInstance
-- 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
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) ≫ (↑U : Y.Opens).ι ≫ g)
⊢ P (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
exact this H inferInstance

Premises used: inferInstance
-- 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
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
wlog : ∀ {X : Scheme.{u}} {f : X ⟶ Y} (h : P (f ≫ g)) (hY : IsAffine X), P f
⊢ P f

Tactic:
wlog hY : IsAffine X generalizing X

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
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
inr : ∀ (i : (↑X.affineOpens : Type u)), P ((↑i : X.Opens).ι ≫ f)
⊢ P f

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

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_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)
inr : ∀ (H : P ((↑U : X.Opens).ι ≫ f ≫ g)), P ((↑U : X.Opens).ι ≫ f)
⊢ P ((↑U : X.Opens).ι ≫ f)

Tactic:
have H := comp_of_isOpenImmersion P U.1.ι (f ≫ g) h
-- 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
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) ≫ g)

Tactic:
rw [← Category.assoc] at H

Premises used: CategoryTheory.Category.assoc
-- 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
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)

Tactic:
this H inferInstance

Premises used: inferInstance
-- 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
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)

Tactic:
exact this H inferInstance

Premises used: inferInstance
-- 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
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
rw :
  ∀ (h : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))) (hY : IsAffine X),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ P f

Tactic:
rw [iff_of_isAffine (P := P)] at h ⊢

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_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 : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))
hY : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
H _ _ h
-- 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
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 : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ g)))
hY : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
exact H _ _ h
-- 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
X Y : Scheme
f : X ⟶ Y
hP : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst_1 : IsOpenImmersion f
⊢ P f

Tactic:
haveI : P.ContainsIdentities := containsIdentities hP
  IsZariskiLocalAtSource.of_isOpenImmersion f

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion
-- 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
hP : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hP' :
  AffineTargetMorphismProperty.IsStableUnderBaseChange.{u}
    (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
⊢ P.IsStableUnderBaseChange

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange
-- 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
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) :=
  ⋯
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)
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u}
    (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- 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
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
hP' :
  ∀ [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)
⊢ ∀ [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:
_