awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
i : J
hi : (↑x : ↥X) ∈ U i
h :
  (PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ } i)
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi) =
    x
⊢ ∃ (i :
    PreZeroHypercover.I₀.{u_1, u_2, u_2 + 1} (C := Scheme) (S := (↑(⨆ (i : J), U i) : Scheme))
      { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ }),
    Membership.mem (γ := Set ↥(↑(⨆ (i : J), U i) : Scheme))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
        ⇑(PreZeroHypercover.f
            { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ :
              PreZeroHypercover.{u_1, u_2, u_2 + 1} (↑(⨆ (i : J), U i) : Scheme) }
            i))
      x

Tactic:
use i, ⟨x.1, hi⟩
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
i : J
hi : (↑x : ↥X) ∈ U i
h :
  (↑((PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ } i)
          (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi)) :
      ↥X) =
    (↑x : ↥X)
⊢ (PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ } i)
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi) =
    x

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
J : Type u_1
X : Scheme
U : J → X.Opens
x : ↥(↑(⨆ (i : J), U i) : Scheme)
i : J
hi : (↑x : ↥X) ∈ U i
⊢ (↑((PreZeroHypercover.f { I₀ := J, X := fun (i : J) ↦ (↑(U i) : Scheme), f := fun (j : J) ↦ X.homOfLE ⋯ } i)
          (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U i) (↑x : ↥X) hi)) :
      ↥X) =
    (↑x : ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U V : X.Opens
i : U ⟶ V
⊢ X.homOfLE ⋯ ≫ (Over.mk V.ι).hom = (Over.mk U.ι).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U : X.Opens
h : Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯) = Over.Hom.left (𝟙 (Over.mk U.ι))
⊢ Over.homMk (X.homOfLE ⋯) ⋯ = 𝟙 (Over.mk U.ι)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U : X.Opens
⊢ Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯) = Over.Hom.left (𝟙 (Over.mk U.ι))

Tactic:
Scheme.homOfLE_rfl _ _

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.IsOpenImmersion.lift, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.homOfLE_rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U : X.Opens
⊢ Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯) = Over.Hom.left (𝟙 (Over.mk U.ι))

Tactic:
exact Scheme.homOfLE_rfl _ _

Premises used: AlgebraicGeometry.Scheme.homOfLE_rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
h :
  Eq.{u + 1} (α := (Over.mk U.ι).left ⟶ (Over.mk W.ι).left) (Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯))
    (Over.Hom.left (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE ⋯) ⋯) (Over.homMk (X.homOfLE ⋯) ⋯)))
⊢ Eq.{u + 1} (α := Over.mk U.ι ⟶ Over.mk W.ι) (Over.homMk (X.homOfLE ⋯) ⋯)
    (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE ⋯) ⋯) (Over.homMk (X.homOfLE ⋯) ⋯))

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Eq.{u + 1} (α := (Over.mk U.ι).left ⟶ (Over.mk W.ι).left) (Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯))
    (Over.Hom.left (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE ⋯) ⋯) (Over.homMk (X.homOfLE ⋯) ⋯)))

Tactic:
(X.homOfLE_homOfLE i.le j.le).symm

Premises used: AlgebraicGeometry.Scheme.homOfLE, Quiver.Hom.le, AlgebraicGeometry.IsOpenImmersion.lift, AlgebraicGeometry.Scheme.homOfLE_homOfLE, AlgebraicGeometry.Scheme.restrict, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 U V W : X.Opens
i : U ⟶ V
j : V ⟶ W
⊢ Eq.{u + 1} (α := (Over.mk U.ι).left ⟶ (Over.mk W.ι).left) (Over.Hom.left (Over.homMk (X.homOfLE ⋯) ⋯))
    (Over.Hom.left (CategoryStruct.comp (Y := Over.mk V.ι) (Over.homMk (X.homOfLE ⋯) ⋯) (Over.homMk (X.homOfLE ⋯) ⋯)))

Tactic:
exact (X.homOfLE_homOfLE i.le j.le).symm

Premises used: Quiver.Hom.le, AlgebraicGeometry.Scheme.homOfLE_homOfLE, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
dsimp :
  Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ X.presheaf.map i
⊢ (X.restrictFunctor.op ⋙ Functor.op (Over.forget X) ⋙ Γ).map i ≫
      Iso.hom ((fun (U : X.Opensᵒᵖ) ↦ Functor.mapIso X.presheaf (Iso.op (Iso.symm (eqToIso ⋯)))) V) =
    Iso.hom ((fun (U : X.Opensᵒᵖ) ↦ Functor.mapIso X.presheaf (Iso.op (Iso.symm (eqToIso ⋯)))) U) ≫ X.presheaf.map i

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
rw :
  X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ i)
⊢ Hom.appTop (X.homOfLE ⋯) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ X.presheaf.map i

Tactic:
rw [X.homOfLE_appTop, ← Functor.map_comp, ← Functor.map_comp]

Premises used: AlgebraicGeometry.Scheme.homOfLE_appTop, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U_1 : X.Opens
U V : X.Opensᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯) ≫ i)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
X : Scheme
U V : X.Opens
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑(U.ι ⁻¹ᵁ V) : Scheme)) ⇑((U.ι ⁻¹ᵁ V).ι ≫ U.ι))
    (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ U) : Scheme)) ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι))

Tactic:
simp only [Hom.comp_base, TopCat.coe_comp, Set.range_comp, Opens.range_ι, Opens.map_coe,
      Set.image_preimage_eq_inter_range, Set.inter_comm (U : Set X)]

Premises used: TopologicalSpace.Opens.map_coe, Set.range_comp, Set.image_preimage_eq_inter_range, Set.inter_comm, SetLike.coe, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U : X.Opens
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(↑U : Scheme)) ⇑(U.ι ≫ f)) (Set.range (ι := ↥(↑(f ''ᵁ U) : Scheme)) ⇑(f ''ᵁ U).ι)

Tactic:
simp [Set.range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : X.Opens
⊢ Iso.hom (isoImage f U) ≫ (f ''ᵁ U).ι = U.ι ≫ f

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : X.Opens
⊢ Iso.inv (isoImage f U) ≫ U.ι ≫ f = (f ''ᵁ U).ι

Tactic:
IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U : X_1.Opens
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(↑(opensRange f) : Scheme)) ⇑(opensRange f).ι)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ Iso.hom (isoOpensRange f) ≫ (opensRange f).ι = f

Tactic:
simp [isoOpensRange]

Premises used: AlgebraicGeometry.Scheme.Hom.isoOpensRange
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ Iso.inv (isoOpensRange f) ≫ f = (opensRange f).ι

Tactic:
simp [isoOpensRange]

Premises used: AlgebraicGeometry.Scheme.Hom.isoOpensRange
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
⊢ X.topIso.inv ≫ Opens.ι ⊤ = 𝟙 X

Tactic:
X.topIso.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.Scheme.topIso
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
⊢ Opens.ι ⊤ ≫ X.topIso.inv = 𝟙 (↑⊤ : Scheme)

Tactic:
X.topIso.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, AlgebraicGeometry.Scheme.topIso
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X_1 : Scheme
U_1 : X_1.Opens
X : Scheme
U V : X.Opens
e : U = V
rw rw₁ : Eq (α := Set ↥X) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι) (Set.range (ι := ↥(↑V : Scheme)) ⇑V.ι)

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U = V
⊢ (X.isoOfEq e).hom ≫ V.ι = U.ι

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U = V
⊢ (X.isoOfEq e).inv ≫ U.ι = V.ι

Tactic:
IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U = V
⊢ (X.isoOfEq e).hom = X.homOfLE ⋯

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.IsOpenImmersion.lift, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
e : U = V
⊢ (X.isoOfEq e).inv = X.homOfLE ⋯

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.homOfLE, AlgebraicGeometry.IsOpenImmersion.lift, rfl
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
w : (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))
⊢ X.isoOfEq ⋯ = Iso.refl (↑U : Scheme)

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U : X.Opens
w : (X.isoOfEq ⋯).hom ≫ U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
w₁ : U.ι = Iso.hom (Iso.refl (↑U : Scheme)) ≫ U.ι
w₂ : U.ι = 𝟙 (↑U : Scheme) ≫ U.ι
w₃ w₄ : U.ι = U.ι
⊢ (X.isoOfEq ⋯).hom = Iso.hom (Iso.refl (↑U : Scheme))

Tactic:
rw [← cancel_mono U.ι, Scheme.isoOfEq_hom_ι, Iso.refl_hom, Category.id_comp]

Premises used: AlgebraicGeometry.Scheme.isoOfEq_hom_ι, CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
apply :
  Eq (α := Set ↥Y) (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑((f ⁻¹ᵁ U).ι ≫ f)) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
⊢ (↑(f ⁻¹ᵁ U) : Scheme) ≅ (↑U : Scheme)

Tactic:
apply IsOpenImmersion.isoOfRangeEq (f := (f ⁻¹ᵁ U).ι ≫ f) U.ι _

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
dsimp :
  Eq (α := Set ↥Y)
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme))
      (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y)
        (⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base) : (a : ↥(↑(f ⁻¹ᵁ U) : Scheme)) → ↥X)))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)
⊢ Eq (α := Set ↥Y) (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme)) ⇑((f ⁻¹ᵁ U).ι ≫ f)) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
rw : (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) '' (↑(f ⁻¹ᵁ U) : Set ↥X) = (↑U : Set ↥Y)
⊢ Eq (α := Set ↥Y)
    (Set.range (ι := ↥(↑(f ⁻¹ᵁ U) : Scheme))
      (Function.comp (β := ↥X) (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y)
        (⇑(TopCat.Hom.hom (f ⁻¹ᵁ U).ι.base) : (a : ↥(↑(f ⁻¹ᵁ U) : Scheme)) → ↥X)))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
rw [Set.range_comp, Opens.range_ι, Opens.range_ι]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
⊢ (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) '' (↑(f ⁻¹ᵁ U) : Set ↥X) = (↑U : Set ↥Y)

Tactic:
@Set.image_preimage_eq _ _ f U.1 f.homeomorph.surjective

Premises used: Set.Mem, setOf, Set.image_preimage_eq, AlgebraicGeometry.Scheme.Hom.homeomorph, TopologicalSpace.Opens.carrier, Set.preimage, Homeomorph.surjective
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst_1 : IsIso f
U : Y.Opens
⊢ (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) '' (↑(f ⁻¹ᵁ U) : Set ↥X) = (↑U : Set ↥Y)

Tactic:
refine @Set.image_preimage_eq _ _ f U.1 f.homeomorph.surjective

Premises used: Set.image_preimage_eq, AlgebraicGeometry.Scheme.Hom.homeomorph, TopologicalSpace.Opens.carrier, Homeomorph.surjective
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Y.Opens
⊢ (preimageIso f U).hom ≫ U.ι = (f ⁻¹ᵁ U).ι ≫ f

Tactic:
IsOpenImmersion.isoOfRangeEq_hom_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_hom_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Y.Opens
⊢ (preimageIso f U).inv ≫ (f ⁻¹ᵁ U).ι ≫ f = U.ι

Tactic:
IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _

Premises used: AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ V.ι ''ᵁ V.ι ⁻¹ᵁ U = U

Tactic:
simpa [Scheme.Hom.image_preimage_eq_opensRange_inf]

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ V.ι ''ᵁ V.ι ⁻¹ᵁ U = U

Tactic:
have : V.ι ''ᵁ (V.ι ⁻¹ᵁ U) = U := by simpa [Scheme.Hom.image_preimage_eq_opensRange_inf]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
rw :
  Set.image (α := ↥(↑V : Scheme)) (⇑V.ι)
      (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Scheme)) ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι) =
    (↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Set ↥X)
⊢ Eq (α := Set ↥X) (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ U) : Scheme)) ⇑((V.ι ⁻¹ᵁ U).ι ≫ V.ι))
    (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Scheme.Opens.range_ι, Set.range_comp, ← this]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
X : Scheme
U V : X.Opens
hUV : U ≤ V
this : V.ι ''ᵁ V.ι ⁻¹ᵁ U = U
⊢ Set.image (α := ↥(↑V : Scheme)) (⇑V.ι)
      (Set.range (ι := ↥(↑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Scheme)) ⇑(V.ι ⁻¹ᵁ V.ι ''ᵁ V.ι ⁻¹ᵁ U).ι) =
    (↑(V.ι ''ᵁ V.ι ⁻¹ᵁ U) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).hom ≫ U.ι = (V.ι ⁻¹ᵁ U).ι ≫ V.ι

Tactic:
simp [isoOfLE]

Premises used: AlgebraicGeometry.Scheme.Opens.isoOfLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι

Tactic:
simp [isoOfLE]

Premises used: AlgebraicGeometry.Scheme.Opens.isoOfLE
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f : (↑R : Type u)
simp :
  (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R)) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
      ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))
⊢ Eq (α := Set ↥(Spec R))
    (Set.range (ι := ↥(↑(PrimeSpectrum.basicOpen f) : Scheme)) ⇑(Scheme.Opens.ι (PrimeSpectrum.basicOpen f)))
    (Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
      ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))

Tactic:
simp only [Scheme.Opens.range_ι]

Premises used: AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f : (↑R : Type u)
⊢ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R)) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
      ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))

Tactic:
(PrimeSpectrum.localization_away_comap_range _ _).symm

Premises used: PrimeSpectrum.comap, Eq.symm, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f : (↑R : Type u)
⊢ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R)) =
    Set.range (ι := ↥(Spec (CommRingCat.of (Localization.Away f))))
      ⇑(Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))

Tactic:
exact (PrimeSpectrum.localization_away_comap_range _ _).symm

Premises used: Eq.symm, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
rw : IsLocalization.Away (f * g) (Localization.Away (f * g))
⊢ IsLocalization.Away (f * g) (Localization.Away x)

Tactic:
rw [hx]
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away (f * g))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
C : Type u₁
inst : Category.{v, u₁} C
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
this : IsLocalization.Away (f * g) (Localization.Away x)
⊢ LE.le (α := (Spec R).Opens) (PrimeSpectrum.basicOpen x) (PrimeSpectrum.basicOpen f)

Tactic:
simp [hx, PrimeSpectrum.basicOpen_mul]

Premises used: PrimeSpectrum.basicOpen_mul
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g x : (↑R : Type u)
hx : x = f * g
subst :
  (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv
⊢ (basicOpenIsoSpecAway x).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv

Tactic:
subst hx
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g : (↑R : Type u)
rw :
  ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)
⊢ (basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯ =
    Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g : (↑R : Type u)
simp :
  Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))
⊢ ((basicOpenIsoSpecAway (f * g)).inv ≫ (Spec R).homOfLE ⋯) ≫ Scheme.Opens.ι (PrimeSpectrum.basicOpen f) =
    (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)) ≫ (basicOpenIsoSpecAway f).inv) ≫
      Scheme.Opens.ι (PrimeSpectrum.basicOpen f)

Tactic:
simp only [basicOpenIsoSpecAway, Category.assoc, Scheme.homOfLE_ι,
    IsOpenImmersion.isoOfRangeEq_inv_fac]

Premises used: AlgebraicGeometry.basicOpenIsoSpecAway, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.IsOpenImmersion.isoOfRangeEq_inv_fac
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g : (↑R : Type u)
simp :
  Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.Away.awayToAwayRight f g) (algebraMap (↑R : Type u) (Localization.Away f)))))
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (IsLocalization.Away.awayToAwayRight f g)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))

Tactic:
simp only [← Spec.map_comp, ← CommRingCat.ofHom_comp]

Premises used: AlgebraicGeometry.Spec.map_comp, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g : (↑R : Type u)
e_f :
  Eq (α := (↑R : Type u) →+* Localization.Away (f * g)) (algebraMap (↑R : Type u) (Localization.Away (f * g)))
    (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
      (algebraMap (↑R : Type u) (Localization.Away f)))
⊢ Eq (α := Spec (CommRingCat.of (Localization.Away (f * g))) ⟶ Spec R)
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away (f * g)))))
    (Spec.map
      (CommRingCat.ofHom
        (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _
          (IsLocalization.Away.awayToAwayRight f g) (algebraMap (↑R : Type u) (Localization.Away f)))))

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.Restrict
Goal:
R : CommRingCat
f g : (↑R : Type u)
e_f :
  ∀ (x : (↑R : Type u)),
    Eq (α := Localization.Away (f * g))
      ((algebraMap (↑R : Type u) (Localization.Away (f * g)) : (a : (↑R : Type u)) → Localization.Away (f * g)) x :
        Localization.Away (f * g))
      ((@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _
              (IsLocalization.Away.awayToAwayRight f g) (algebraMap (↑R : Type u) (Localization.Away f)) :
            (a : (↑R : Type u)) → Localization.Away (f * g))
          x :
        Localization.Away (f * g))
⊢ Eq (α := (↑R : Type u) →+* Localization.Away (f * g)) (algebraMap (↑R : Type u) (Localization.Away (f * g)))
    (@RingHom.comp _ (Localization.Away f) _ _ Semiring.toNonAssocSemiring _ (IsLocalization.Away.awayToAwayRight f g)
      (algebraMap (↑R : Type u) (Localization.Away f)))

Tactic:
ext x