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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
have refine_1 : P (f ≫ Y.isoSpec.hom)
Tactic: rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
-- 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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
have w : CommRingCat
Tactic: use Γ(Y, ⊤), Γ(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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
w w₁ : CommRingCat
⊢ ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
have h : Spec Γ(Y, ⊤) = Spec Γ(Y, ⊤) ∧ Spec Γ(X, ⊤) = Spec Γ(X, ⊤)
Tactic: use Γ(Y, ⊤), Γ(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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : ∀
  (this :
    Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))),
  Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: have : Q' ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom).stalkMap (X.isoSpec.hom x)).hom := by
      refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_
      · rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
      · use Γ(Y, ⊤), Γ(X, ⊤)
-- 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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have this₁ : Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
Tactic: rw [Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp,
      hQ'.cancel_right_isIso, CommRingCat.hom_comp, hQ'.cancel_left_isIso] at this
Cleared hypotheses: this
-- 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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have heq : X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x
Tactic: have heq : (X.isoSpec.inv (X.isoSpec.hom x)) = x := by simp
-- 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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this_1 :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
this :
  Q' (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) : ↥X))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))))))
heq : X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : ∀ (this : Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
  (heq : X.isoSpec.inv (X.isoSpec.hom x : ↥(Spec Γ(X, ⊤))) = x), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: rwa [hQ'.arrow_mk_iso_iff (f.arrowStalkMapIsoOfEq heq)] at this
Cleared hypotheses: this, heq
-- 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
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have obtain : ∀ (R S : CommRingCat.{u}) (hY : IsAffine.{u} (Spec R)) (x : ↥(Spec S)) (hX : IsAffine.{u} (Spec S))
  {f : Spec S ⟶ Spec R} (hf : P f), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: obtain ⟨R, S, rfl, rfl⟩ := hXY
Cleared hypotheses: X, Y, f, hf, x, hX, hY, hXY
-- 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
X Y : Scheme
f_1 : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
f : Spec S ⟶ Spec R
hf : P f
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have obtain : ∀ (φ : R ⟶ S) (hf : P (Spec.map φ)), Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: 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
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
have rw : Q' (R := (↑(CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal)) : Type u))
  (S := (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
        (CommRingCat.Hom.hom φ) sorry)))
Tactic: rw [hQ'.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]
-- 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
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
x : ↥(Spec S)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
hf : P (Spec.map φ)
⊢ Q' (R := (↑(CommRingCat.of (Localization.AtPrime (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal)) : Type u))
    (S := (↑(CommRingCat.of (Localization.AtPrime x.asIdeal)) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) x).asIdeal x.asIdeal
          (CommRingCat.Hom.hom φ) ⋯)))
have hf₁ : Q (CommRingCat.Hom.hom φ)
Tactic: rw [Spec_iff (P := P)] at hf
Cleared hypotheses: 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
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S), Q f ↔ Q' f
⊢ P = P'
have h₁ : ∀ ⦃f Y : Scheme.{u}⦄ (f_1 : f ⟶ Y), P f_1 ↔ P' f_1
Tactic: ext f
-- 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
P' : MorphismProperty Scheme
Q' : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
h : ∀ {R S : Type u} [inst : CommRing R] [inst_2 : CommRing S] (f : R →+* S), Q f ↔ Q' f
f Y : Scheme
f_1 : f ⟶ Y
⊢ P f_1 ↔ P' f_1
have h₁ : (∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))) ↔
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑f.affineOpens : Type u)) (e : (↑V : f.Opens) ≤ f_1 ⁻¹ᵁ (↑U : Y.Opens)),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f_1 (↑U : Y.Opens) (↑V : f.Opens) e))
Tactic: rw [HasRingHomProperty.eq_affineLocally (P := P), HasRingHomProperty.eq_affineLocally (P := P'),
    affineLocally_iff_affineOpens_le, affineLocally_iff_affineOpens_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
⊢ IsDominant f
have rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
⊢ IsDominant f
have rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
⊢ IsDominant f
have rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
⊢ IsDominant f
have rw₃ : (↑(Scheme.Hom.ker f).support : Set ↥S) = Set.univ
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
rw₃ : (↑(Scheme.Hom.ker f).support : Set ↥S) = Set.univ
⊢ IsDominant f
have rw₄ : (↑(Scheme.IdealSheafData.support ⊥) : Set ↥S) = Set.univ
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
rw₃ : (↑(Scheme.Hom.ker f).support : Set ↥S) = Set.univ
rw₄ : (↑(Scheme.IdealSheafData.support ⊥) : Set ↥S) = Set.univ
⊢ IsDominant f
have rw₅ : (↑⊤ : Set ↥S) = Set.univ
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsSchemeTheoreticallyDominant f
inst_1 : QuasiCompact f
rw : DenseRange (X := ↥S) (α := ↥X) ⇑f
rw₁ : Dense (X := ↥S) (Set.range (ι := ↥X) ⇑f)
rw₂ : Eq (α := Set ↥S) (closure (Set.range (ι := ↥X) ⇑f)) Set.univ
rw₃ : (↑(Scheme.Hom.ker f).support : Set ↥S) = Set.univ
rw₄ : (↑(Scheme.IdealSheafData.support ⊥) : Set ↥S) = Set.univ
rw₅ : (↑⊤ : Set ↥S) = Set.univ
⊢ IsDominant f
have rw₆ : Eq.{u_1 + 1} (α := Set ↥S) Set.univ Set.univ
Tactic: rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
⊢ IsSchemeTheoreticallyDominant (f ≫ g)
have rw : Scheme.Hom.ker (f ≫ g) = ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
rw : Scheme.Hom.ker (f ≫ g) = ⊥
⊢ IsSchemeTheoreticallyDominant (f ≫ g)
have rw₁ : (Scheme.Hom.ker f).map g = ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
rw : Scheme.Hom.ker (f ≫ g) = ⊥
rw₁ : (Scheme.Hom.ker f).map g = ⊥
⊢ IsSchemeTheoreticallyDominant (f ≫ g)
have rw₂ : Scheme.IdealSheafData.map ⊥ g = ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
rw : Scheme.Hom.ker (f ≫ g) = ⊥
rw₁ : (Scheme.Hom.ker f).map g = ⊥
rw₂ : Scheme.IdealSheafData.map ⊥ g = ⊥
⊢ IsSchemeTheoreticallyDominant (f ≫ g)
have rw₃ : Scheme.Hom.ker g = ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant (goal)
Goal:
X Y Z S : Scheme
f_1 : X ⟶ S
g_1 : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst : IsSchemeTheoreticallyDominant f
inst_1 : IsSchemeTheoreticallyDominant g
rw : Scheme.Hom.ker (f ≫ g) = ⊥
rw₁ : (Scheme.Hom.ker f).map g = ⊥
rw₂ : Scheme.IdealSheafData.map ⊥ g = ⊥
rw₃ : Scheme.Hom.ker g = ⊥
⊢ IsSchemeTheoreticallyDominant (f ≫ g)
have rw₄ : Eq.{u_1 + 1} (α := Z.IdealSheafData) ⊥ ⊥
Tactic: rw [isSchemeTheoreticallyDominant_iff, Scheme.Hom.ker_comp, f.ker_eq_bot,
    Scheme.IdealSheafData.map_bot, g.ker_eq_bot]