awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
a :
  Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u)) →
    Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))
a₁ :
  Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u)) →
    Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) Set.univ
⊢ Eq (α := Set ↥(Spec Γ(X, U)))
      (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
      (⇑hU.fromSpec ⁻¹' U.carrier) ↔
    Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ

Tactic:
congr! 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
⊢ Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
    (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))

Tactic:
congr_arg (Set.iUnion ·) ?_

Premises used: congr_arg, Set.iUnion
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
a :
  Eq.{u + 1} (α := (↑s : Type u) → Set ↥(Spec Γ(X, U)))
    (fun (i : (↑s : Type u)) ↦ ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    fun (i : (↑s : Type u)) ↦ Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))
⊢ Eq.{u + 1} (α := Set ↥(Spec Γ(X, U)))
    (⋃ (i : (↑s : Type u)), ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u))))

Tactic:
refine congr_arg (Set.iUnion ·) ?_

Premises used: congr_arg, Set.iUnion
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
a :
  ∀ (x : (↑s : Type u)),
    Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑x : (↑Γ(X, U) : Type u))) : Set ↥X))
      (Opens.carrier (PrimeSpectrum.basicOpen (↑x : (↑Γ(X, U) : Type u))))
⊢ Eq.{u + 1} (α := (↑s : Type u) → Set ↥(Spec Γ(X, U)))
    (fun (i : (↑s : Type u)) ↦ ⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑i : (↑Γ(X, U) : Type u))) : Set ↥X))
    fun (i : (↑s : Type u)) ↦ Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))

Tactic:
ext1 x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
x : (↑s : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑x : (↑Γ(X, U) : Type u))) : Set ↥X))
    (Opens.carrier (PrimeSpectrum.basicOpen (↑x : (↑Γ(X, U) : Type u))))

Tactic:
congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)

Premises used: Set.Mem, setOf, TopologicalSpace.Opens.carrier, congr_arg, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
x : (↑s : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen (↑x : (↑Γ(X, U) : Type u))) : Set ↥X))
    (Opens.carrier (PrimeSpectrum.basicOpen (↑x : (↑Γ(X, U) : Type u))))

Tactic:
exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)

Premises used: TopologicalSpace.Opens.carrier, congr_arg, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) Set.univ

Tactic:
congr_arg Opens.carrier hU.fromSpec_preimage_self

Premises used: Set.Mem, Set.univ, setOf, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, TopologicalSpace.Opens.carrier, congr_arg, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
e_1 : Set ↥(Spec Γ(X, U)) = Set (PrimeSpectrum (↑Γ(X, U) : Type u))
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' U.carrier) Set.univ

Tactic:
exact congr_arg Opens.carrier hU.fromSpec_preimage_self

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self, TopologicalSpace.Opens.carrier, congr_arg
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
simp :
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), (PrimeSpectrum.zeroLocus {(↑i : (↑Γ(X, U) : Type u))})ᶜ) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), Opens.carrier (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, U) : Type u)))) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤

Tactic:
simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]

Premises used: TopologicalSpace.Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
rw :
  Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (PrimeSpectrum.zeroLocus (⋃ (i : (↑s : Type u)), {(↑i : (↑Γ(X, U) : Type u))})) ∅ ↔
    Eq (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u))) (PrimeSpectrum.zeroLocus s) ∅
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (⋃ (i : (↑s : Type u)), (PrimeSpectrum.zeroLocus {(↑i : (↑Γ(X, U) : Type u))})ᶜ) Set.univ ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤

Tactic:
rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
      PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]

Premises used: Set.compl_iInter, PrimeSpectrum.zeroLocus_span, PrimeSpectrum.zeroLocus_iUnion, PrimeSpectrum.zeroLocus_empty_iff_eq_top, Set.compl_univ_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u)))
      (PrimeSpectrum.zeroLocus (⋃ (i : (↑s : Type u)), {(↑i : (↑Γ(X, U) : Type u))})) ∅ ↔
    Eq (α := Set (PrimeSpectrum (↑Γ(X, U) : Type u))) (PrimeSpectrum.zeroLocus s) ∅

Tactic:
simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.setOf_mem_eq]

Premises used: Set.iUnion_singleton_eq_range, Set.setOf_mem_eq, Subtype.range_val_subtype
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
rw :
  U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    U = ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
⊢ U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤

Tactic:
rw [← hU.iSup_basicOpen_eq_self_iff, @comm _ Eq]

Premises used: comm, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
⊢ U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    U = ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))

Tactic:
⟨fun h => le_antisymm h ?_, le_of_eq⟩

Premises used: le_antisymm, Iff.intro, le_of_eq
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
refine :
  ∀ (h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))),
    ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ≤ U
⊢ U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ↔
    U = ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))

Tactic:
refine ⟨fun h => le_antisymm h ?_, le_of_eq⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
simp : ∀ (x : (↑Γ(X, U) : Type u)) (h : x ∈ s), X.basicOpen x ≤ U
⊢ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u)) ≤ U

Tactic:
simp only [iSup_le_iff, SetCoe.forall]

Premises used: iSup_le_iff, SetCoe.forall
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
x : (↑Γ(X, U) : Type u)
_ : x ∈ s → X.basicOpen x ≤ U
⊢ ∀ (h : x ∈ s), X.basicOpen x ≤ U

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
x : (↑Γ(X, U) : Type u)
h_1 : x ∈ s
⊢ X.basicOpen x ≤ U

Tactic:
X.basicOpen_le x

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h : U ≤ ⨆ (f : (↑s : Type u)), X.basicOpen (↑f : (↑Γ(X, U) : Type u))
x : (↑Γ(X, U) : Type u)
h_1 : x ∈ s
⊢ X.basicOpen x ≤ U

Tactic:
exact X.basicOpen_le x

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
refine_1 :
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left
refine_2 :
  (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right
refine_3 :
  Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
      (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom
⊢ Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r) ≅
    Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

Tactic:
refine Arrow.isoMk ?_ ?_ ?_

Premises used: CategoryTheory.Arrow.isoMk
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
⊢ (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).left

Tactic:
exact (Spec _).isoOfEq (comap_basicOpen _ _) ≪≫
      (IsAffineOpen.Spec_basicOpen (f.hom r)).isoSpec ≪≫ Scheme.Spec.mapIso e₂.toCommRingCatIso.op

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Spec, CommRingCat.Hom.hom, CategoryTheory.Iso.op, RingEquiv.toCommRingCatIso, AlgebraicGeometry.Scheme.Spec, PrimeSpectrum.comap_basicOpen, AlgebraicGeometry.Scheme.isoOfEq, AlgEquiv.toRingEquiv, DFunLike.coe, CategoryTheory.Functor.mapIso, AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
⊢ (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).right ≅
    (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).right

Tactic:
exact (IsAffineOpen.Spec_basicOpen r).isoSpec ≪≫ Scheme.Spec.mapIso e₁.toCommRingCatIso.op

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, CategoryTheory.Iso.op, RingEquiv.toCommRingCatIso, AlgebraicGeometry.Scheme.Spec, AlgEquiv.toRingEquiv, CategoryTheory.Functor.mapIso, AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
⊢ IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))

Tactic:
have := AlgebraicGeometry.IsOpenImmersion.of_isLocalization
      (S := (Localization.Away r)) r
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
refine_3 :
  Eq (α :=
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ⟶
      Spec (CommRingCat.of (↑R : Type u_1)))
    ((Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
    (((Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
        (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
⊢ Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
      (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom =
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
      (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom

Tactic:
rw [← cancel_mono (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away r))))]

Premises used: CommRingCat.carrier, Algebra.algebraMap, Localization.Away, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
refine_3 :
  Eq (α := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme) ⟶ Spec (CommRingCat.of (↑R : Type u_1)))
    (Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom))
    (Spec.map f ∣_ basicOpen r ≫
      ⋯.isoSpec.hom ≫
        Spec.map
          (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom))
⊢ Eq (α :=
    (Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).left ⟶
      Spec (CommRingCat.of (↑R : Type u_1)))
    ((Iso.hom ((Spec S).isoOfEq ⋯ ≪≫ IsAffineOpen.isoSpec ⋯ ≪≫ Scheme.Spec.mapIso e₂.toRingEquiv.toCommRingCatIso.op) ≫
        (Arrow.mk (Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
    (((Arrow.mk (X := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme)) (Spec.map f ∣_ basicOpen r)).hom ≫
        (⋯.isoSpec ≪≫ Scheme.Spec.mapIso e₁.toRingEquiv.toCommRingCatIso.op).hom) ≫
      Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))

Tactic:
simp only [Arrow.mk_left, Arrow.mk_right, Scheme.isoOfEq_rfl, Iso.refl_trans,
      Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Scheme.Spec_map, Quiver.Hom.unop_op,
      Arrow.mk_hom, Category.assoc, ← Spec.map_comp]

Premises used: CategoryTheory.Category.assoc, Quiver.Hom.unop_op, CategoryTheory.Iso.op_hom, CategoryTheory.Arrow.mk_right, CategoryTheory.Iso.refl_trans, CategoryTheory.Arrow.mk_hom, AlgebraicGeometry.Scheme.isoOfEq_rfl, CategoryTheory.Iso.trans_hom, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Arrow.mk_left, AlgebraicGeometry.Scheme.Spec_map, CategoryTheory.Functor.mapIso_hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
a :
  Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
        CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom)
a₁ :
  Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
| Eq (α := (↑(Spec.map f ⁻¹ᵁ basicOpen r) : Scheme) ⟶ Spec (CommRingCat.of (↑R : Type u_1)))
    (Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫
          CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r) ≫ e₂.toRingEquiv.toCommRingCatIso.hom))
    (Spec.map f ∣_ basicOpen r ≫
      ⋯.isoSpec.hom ≫
        Spec.map
          (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom))

Tactic:
congr