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_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
      (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
⊢ ∃ (T : Type u) (x : CommRing T) (x_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) T) (_ :
    IsLocalization.Away (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u)) T),
    Q (R := (↑Γ(Y, ⊤) : Type u))
      (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u)) (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) T)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)))
have openCover : Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
  (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)))
Tactic: refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
-- 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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H_1 : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
U : (↑X.affineOpens : Type u)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u)
hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤
H :
  ∀ (f_1 : ↥s),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
      (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom
        (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) ⋯))
r : (↑(↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
    (RingHom.comp (β := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u)
        (↑Γ(X, X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)))
have openCover : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (X.basicOpen (↑r : (↑Γ(X, (↑U : X.Opens)) : Type u))) sorry))
Tactic: rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(S i) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(S i) : X.Opens) ⋯))
have H₁ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
Tactic: specialize H i
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
H : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(S i) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(S i) : X.Opens) ⋯))
have H₁ : Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
  (↑Γ((↑(↑(S i) : X.Opens) : Scheme), (IsOpenImmersion.isoOfRangeEq (𝒰.f i) (↑(S i) : X.Opens).ι sorry).inv ⁻¹ᵁ ⊤) :
    Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(S i) : X.Opens).ι ''ᵁ ⊤) sorry))
Tactic: rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
      ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.comp_appTop,
      Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] 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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : (↑X.affineOpens : Type u)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
have basicOpen : ∀ (U : (↑X.affineOpens : Type u)) (r : (↑Γ(X, (↑U : X.Opens)) : Type u))
  (H :
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry))),
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(X.affineBasicOpen r) : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen r) : X.Opens) sorry))
Tactic: induction U using of_affine_open_cover S 𝒰.iSup_opensRange with
  | basicOpen U r H =>
    simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
    have := U.2.isLocalization_basicOpen r
    exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H
  | openCover U s hs H =>
    apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
      (isLocal_ringHomProperty P).respectsIso _ _ hs
    rintro r
    refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
    rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
    exact H r
  | hU i =>
    specialize H i
    rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
      ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.comp_appTop,
      Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H
    exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H
Cleared hypotheses: U
-- 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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : Scheme.OpenCover.{u_1, u} X
inst_2 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
H : ∀ (i : 𝒰.I₀), Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.f i ≫ f)))
U : (↑X.affineOpens : Type u)
S : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (r : (↑Γ(X, (↑U : X.Opens)) : Type u))
    (H :
      Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(X.affineBasicOpen r) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen r) : X.Opens) ⋯))
⊢ Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
have openCover : ∀ (U : (↑X.affineOpens : Type u)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u))
  (hs : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊤)
  (H :
    ∀ (f_1 : ↥s),
      Q (R := (↑Γ(Y, ⊤) : Type u)) (S :=
        (↑Γ(X, (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens)) : Type u))
        (CommRingCat.Hom.hom
          (Scheme.Hom.appLE f ⊤ (↑(X.affineBasicOpen (↑f_1 : (↑Γ(X, (↑U : X.Opens)) : Type u))) : X.Opens) sorry))),
  Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry))
Tactic: induction U using of_affine_open_cover S 𝒰.iSup_opensRange with
  | basicOpen U r H =>
    simp_rw [Scheme.affineBasicOpen_coe,
      ← f.appLE_map (U := ⊤) le_top (homOfLE (X.basicOpen_le r)).op]
    have := U.2.isLocalization_basicOpen r
    exact (isLocal_ringHomProperty P).StableUnderCompositionWithLocalizationAwayTarget _ r _ H
  | openCover U s hs H =>
    apply (isLocal_ringHomProperty P).ofLocalizationSpanTarget.ofIsLocalization
      (isLocal_ringHomProperty P).respectsIso _ _ hs
    rintro r
    refine ⟨_, _, _, IsAffineOpen.isLocalization_basicOpen U.2 r, ?_⟩
    rw [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp, Scheme.Hom.appLE_map]
    exact H r
  | hU i =>
    specialize H i
    rw [← (isLocal_ringHomProperty P).respectsIso.cancel_right_isIso _
      ((IsOpenImmersion.isoOfRangeEq (𝒰.f i) (S i).1.ι
      Subtype.range_coe.symm).inv.app _), ← CommRingCat.hom_comp, ← Scheme.Hom.comp_appTop,
      IsOpenImmersion.isoOfRangeEq_inv_fac_assoc, Scheme.Hom.comp_appTop,
      Scheme.Opens.ι_appTop, Scheme.Hom.appTop, Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_map] at H
    exact (f.appLE_congr _ rfl (by simp) (fun f => Q f.hom)).mp H
Cleared hypotheses: U
-- 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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine X
inst_2 : IsAffine Y
⊢ P f ↔ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
have rw : (∀
    (i :
      (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
          (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).I₀),
    Q
      (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          ((Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  (Scheme.coverOfIsIso (P := IsOpenImmersion) (𝟙 X))).f
              i ≫
            f)))) ↔
  Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
Tactic: rw [iff_of_source_openCover (P := P) (Scheme.coverOfIsIso.{u} (𝟙 _))]
-- 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
R S : CommRingCat
φ : R ⟶ S
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Tactic: have H := (isLocal_ringHomProperty P).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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw₁ : Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
  Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
rw₁ :
  Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw₂ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
rw₁ :
  Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
rw₂ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw₃ : Q (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ φ)) ↔ Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
rw₁ :
  Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
rw₂ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)
rw₃ : Q (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ φ)) ↔ Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw₄ : Q ((CommRingCat.Hom.hom φ).comp (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).hom)) ↔ Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
R S : CommRingCat
φ : R ⟶ S
H : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ))) ↔ Q (CommRingCat.Hom.hom φ)
rw₁ :
  Q ((CommRingCat.Hom.hom (Scheme.ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ)))) ↔
    Q (CommRingCat.Hom.hom φ)
rw₂ : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map φ) ≫ (Scheme.ΓSpecIso S).hom)) ↔ Q (CommRingCat.Hom.hom φ)
rw₃ : Q (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).hom ≫ φ)) ↔ Q (CommRingCat.Hom.hom φ)
rw₄ : Q ((CommRingCat.Hom.hom φ).comp (CommRingCat.Hom.hom (Scheme.ΓSpecIso R).hom)) ↔ Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
have rw₅ : Q (CommRingCat.Hom.hom φ) ↔ Q (CommRingCat.Hom.hom φ)
Tactic: rw [iff_of_isAffine (P := P), ← H.cancel_right_isIso _ (Scheme.ΓSpecIso _).hom,
    ← CommRingCat.hom_comp, Scheme.ΓSpecIso_naturality, CommRingCat.hom_comp, H.cancel_left_isIso]
-- 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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
⊢ P f
have have : ∀
  (this :
    ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
      IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)),
  P f
Tactic: have (i : _) : IsAffine ((X.openCoverOfIsOpenCover _ hU).X i) := (U i).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
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H :
  ∀ (i : ι),
    Q (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑(U i) : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑(U i) : X.Opens) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
    IsAffine.{u} ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).X i)
⊢ P f
have refine : ∀ (i : (X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).I₀),
  Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun (i : ι) ↦ (↑(U i) : X.Opens)) hU).f i ≫ f)))
Tactic: refine of_source_openCover (X.openCoverOfIsOpenCover _ hU) fun i ↦ ?_
-- 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 Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource P
have H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
  sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
Tactic: apply HasAffineProperty.isZariskiLocalAtSource
-- 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
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
inst_1 : IsAffine Y
𝒰 : X.OpenCover
⊢ sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
have H : (∀ (i : 𝒰.affineRefinement.openCover.I₀),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝒰.affineRefinement.openCover.f i ≫ f)))) ↔
  ∀ (i : 𝒰.I₀)
    (i_1 : PreZeroHypercover.I₀ (S := 𝒰.X i) (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover)),
    Q
      (CommRingCat.Hom.hom
        (Scheme.Hom.appTop
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (𝒰.X i).affineCover) i_1 ≫ 𝒰.f i ≫ f)))
Tactic: simp_rw [← HasAffineProperty.iff_of_isAffine (P := P),
    iff_of_source_openCover 𝒰.affineRefinement.openCover,
    fun i ↦ iff_of_source_openCover (P := P) (f := 𝒰.f i ≫ f) (𝒰.X i).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.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
⊢ P (𝟙 X)
have rw : ∀ (i : (↑X.affineOpens : Type u)), P (X := (↑(𝟙 X ⁻¹ᵁ (↑i : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑i : X.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.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : (↑X.affineOpens : Type u)
⊢ P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))
have have : ∀ (this : IsAffine.{u} (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)),
  P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))
Tactic: have : IsAffine (𝟙 X ⁻¹ᵁ U.1) := U.2
-- 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.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : (↑X.affineOpens : Type u)
this : IsAffine.{u} (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)
⊢ P (X := (↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (𝟙 X ∣_ (↑U : X.Opens))
have rw : Q (CommRingCat.Hom.hom (𝟙 Γ((↑(𝟙 X ⁻¹ᵁ (↑U : X.Opens)) : Scheme), ⊤)))
Tactic: rw [morphismRestrict_id, iff_of_isAffine (P := P), Scheme.Hom.id_appTop]