awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁) =
    Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂

Tactic:
Opens.ext (IsOpenImmersion.range_pullback_to_base_of_left _ _)

Premises used: TopologicalSpace.Opens.ext, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁) =
    Scheme.Hom.opensRange f₁ ⊓ Scheme.Hom.opensRange f₂

Tactic:
exact Opens.ext (IsOpenImmersion.range_pullback_to_base_of_left _ _)

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ IsAffineOpen (Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))

Tactic:
have : IsAffineOpen (pullback.fst f₁ f₂ ≫ f₁).opensRange := by
      convert! H _ _ (isAffineOpen_opensRange f₁) (isAffineOpen_opensRange f₂) using 1
      exact Opens.ext (IsOpenImmersion.range_pullback_to_base_of_left _ _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
this : IsAffineOpen (Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁))
⊢ IsAffine.{u} (↑(Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁)) : Scheme)

Tactic:
change IsAffine _ at this

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
this : IsAffine.{u} (↑(Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁)) : Scheme)
⊢ IsAffine.{u} (pullback f₁ f₂)

Tactic:
.of_isIso (pullback.fst f₁ f₂ ≫ f₁).isoOpensRange.hom

Premises used: AlgebraicGeometry.Scheme.Hom.isoOpensRange, AlgebraicGeometry.IsAffine.of_isIso, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : X.Opens), IsAffineOpen U → IsAffineOpen V → IsAffineOpen (U ⊓ V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
this : IsAffine.{u} (↑(Scheme.Hom.opensRange (X := pullback f₁ f₂) (pullback.fst f₁ f₂ ≫ f₁)) : Scheme)
⊢ IsAffine.{u} (pullback f₁ f₂)

Tactic:
exact .of_isIso (pullback.fst f₁ f₂ ≫ f₁).isoOpensRange.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsAffineHom (Y := pullback.diagonalObj f) (pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
congr($(HasAffineProperty.eq_targetAffineLocally
    (.diagonal @IsAffineHom)) f).to_iff.trans ?_

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.IsAffineHom, congrArg, Eq.to_iff, id, Iff.trans, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
refine :
  targetAffineLocally
      (AffineTargetMorphismProperty.diagonal fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ IsAffineHom (Y := pullback.diagonalObj f) (pullback.diagonal f) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
refine congr($(HasAffineProperty.eq_targetAffineLocally
    (.diagonal @IsAffineHom)) f).to_iff.trans ?_

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.IsAffineHom, congrArg, Eq.to_iff, id, Iff.trans, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
simp :
  (∀ (a : Y.Opens) (b : IsAffineOpen a) (a_1 : X.Opens) (b : a_1 ≤ f ⁻¹ᵁ a) (a_2 : X.Opens) (b : a_2 ≤ f ⁻¹ᵁ a),
      IsAffineOpen (f ⁻¹ᵁ a ⊓ a_1) → IsAffineOpen (f ⁻¹ᵁ a ⊓ a_2) → IsAffineOpen (f ⁻¹ᵁ a ⊓ (a_1 ⊓ a_2))) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ targetAffineLocally
      (AffineTargetMorphismProperty.diagonal fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ IsAffine X) f ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
simp only [targetAffineLocally, diagonal_isAffine_iff_forall_isAffineOpen_inf,
    (IsOpenImmersion.opensEquiv (f ⁻¹ᵁ _).ι).forall_congr_left, Scheme.affineOpens,
    Subtype.forall, Set.mem_setOf_eq, Scheme.Opens.opensRange_ι, ← Scheme.Hom.preimage_inf,
    IsOpenImmersion.opensEquiv_symm_apply, Scheme.Hom.image_preimage_eq_opensRange_inf,
    ← Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (Scheme.Opens.ι _)]

Premises used: AlgebraicGeometry.IsOpenImmersion.opensEquiv, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Opens.opensRange_ι, Equiv.forall_congr_left, Subtype.forall, Set.mem_setOf_eq, AlgebraicGeometry.diagonal_isAffine_iff_forall_isAffineOpen_inf, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.IsOpenImmersion.opensEquiv_symm_apply, AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.Scheme.Hom.preimage_inf, AlgebraicGeometry.Scheme.affineOpens, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
a :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U) (V₁ : X.Opens) (hV₁ : V₁ ≤ f ⁻¹ᵁ U) (V₂ : X.Opens) (hV₂ : V₂ ≤ f ⁻¹ᵁ U),
    IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
      IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ (∀ (a : Y.Opens) (b : IsAffineOpen a) (a_1 : X.Opens) (b : a_1 ≤ f ⁻¹ᵁ a) (a_2 : X.Opens) (b : a_2 ≤ f ⁻¹ᵁ a),
      IsAffineOpen (f ⁻¹ᵁ a ⊓ a_1) → IsAffineOpen (f ⁻¹ᵁ a ⊓ a_2) → IsAffineOpen (f ⁻¹ᵁ a ⊓ (a_1 ⊓ a_2))) ↔
    ∀ (U : Y.Opens),
      IsAffineOpen U → ∀ V₁ ≤ f ⁻¹ᵁ U, ∀ V₂ ≤ f ⁻¹ᵁ U, IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
congr! with U hU V₁ hV₁ V₂ hV₂
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V₁ : X.Opens
hV₁ : V₁ ≤ f ⁻¹ᵁ U
V₂ : X.Opens
hV₂ : V₂ ≤ f ⁻¹ᵁ U
a :
  IsAffineOpen V₁ → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
a₁ :
  IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
a₂ a₃ :
  IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)
⊢ IsAffineOpen (f ⁻¹ᵁ U ⊓ V₁) → IsAffineOpen (f ⁻¹ᵁ U ⊓ V₂) → IsAffineOpen (f ⁻¹ᵁ U ⊓ (V₁ ⊓ V₂)) ↔
    IsAffineOpen V₁ → IsAffineOpen V₂ → IsAffineOpen (V₁ ⊓ V₂)

Tactic:
rw [inf_eq_right.mpr hV₁, inf_eq_right.mpr hV₂, inf_eq_right.mpr (inf_le_left.trans hV₁)]

Premises used: Iff.mpr, inf_le_left, LE.le.trans, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
inst : IsAffineHom (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X)) (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ U ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
inst : IsAffineHom (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X)) (pullback.diagonal (terminal.from X))
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
⊢ V ≤ terminal.from X ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
inst : IsAffineHom (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X)) (pullback.diagonal (terminal.from X))
ι : Sort u_1
inst_1 : Finite ι
inst_2 : Nonempty ι
U : ι → X.Opens
hU : ∀ (i : ι), IsAffineOpen (U i)
⊢ IsAffineOpen.{u} (X := X) (⨅ (i : ι), U i)

Tactic:
InfClosed.iInf_mem_of_nonempty (s := setOf IsAffineOpen) (fun _ h _ h' ↦ h.inf h') hU

Premises used: Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen, InfClosed.iInf_mem_of_nonempty, AlgebraicGeometry.IsAffineOpen.inf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
inst : IsAffineHom (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X)) (pullback.diagonal (terminal.from X))
ι : Type u_1
s : Set ι
hs : s.Finite
hs' : s.Nonempty
U : ι → X.Opens
hU : ∀ i ∈ s, IsAffineOpen (U i)
⊢ IsAffineOpen.{u} (X := X) (⨅ i ∈ s, U i)

Tactic:
InfClosed.biInf_mem_of_nonempty (s := setOf IsAffineOpen) (fun _ h _ h' ↦ h.inf h') hs hs' hU

Premises used: Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen, InfClosed.biInf_mem_of_nonempty, AlgebraicGeometry.IsAffineOpen.inf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    IsAffine X ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
Iff.rfl

Premises used: Iff.rfl, AlgebraicGeometry.affineAnd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso

Tactic:
RespectsIso.mk _ ?_ ?_

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
refine_1 :
  ∀ {X Y Z : Scheme.{u}} (e : X ≅ Y) (f : Y ⟶ Z),
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
refine_2 :
  ∀ {X Y Z : Scheme.{u}} (e : Y ≅ Z) (f : X ⟶ Y),
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
      (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso

Tactic:
refine RespectsIso.mk _ ?_ ?_

Premises used: CategoryTheory.MorphismProperty.RespectsIso.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
refine_1 :
  ∀ (hZ : IsAffine Z) (hY : IsAffine Y) (hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))),
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)

Tactic:
⟨hZ, ⟨hY, hf⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : X ≅ Y
f : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (e.hom ≫ f)

Tactic:
simpa [hP.cancel_right_isIso, IsAffine.of_isIso e.hom]

Premises used: AlgebraicGeometry.IsAffine.of_isIso, RingHom.RespectsIso.cancel_right_isIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
refine_2 :
  ∀ (hZ : IsAffine Y) (hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f),
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty f →
    (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
⟨hZ, hf⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
e : Y ≅ Z
f : X ⟶ Y
hZ : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty (f ≫ e.hom)

Tactic:
simpa [AffineTargetMorphismProperty.toProperty, IsAffine.of_isIso e.inv, hP.cancel_left_isIso]

Premises used: AlgebraicGeometry.IsAffine.of_isIso, RingHom.RespectsIso.cancel_left_isIso, AlgebraicGeometry.AffineTargetMorphismProperty.toProperty, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
right :
  (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u)
    _ _ _ (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))
⊢ affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
    (f ∣_ Y.basicOpen r)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
left :
  IsAffine.{u}
    (↑(X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r)) :
      Scheme)
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)

Tactic:
simp only [Scheme.preimage_basicOpen, Opens.map_top]

Premises used: TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine.{u}
    (↑(X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r)) :
      Scheme)

Tactic:
(isAffineOpen_top X).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.IsAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ IsAffine.{u}
    (↑(X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r)) :
      Scheme)

Tactic:
exact (isAffineOpen_top X).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right :
  Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u)
    _ _ _ (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))

Tactic:
dsimp only
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right :
  Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))
⊢ Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen r)))

Tactic:
rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.morphismRestrict_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right :
  Q (R := (↑Γ(Y, (Y.basicOpen r).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))
⊢ Q (R := (↑Γ((↑(Y.basicOpen r) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))

Tactic:
change Q (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)).hom

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.Scheme.Opens.ι, Top.top, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right : Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
⊢ Q (R := (↑Γ(Y, (Y.basicOpen r).ι ''ᵁ ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen r).ι ''ᵁ ⊤)))

Tactic:
rw [Scheme.Opens.ι_image_top]

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top