awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
hUV : Eq.{u + 1} (α := Y.Opens) ((fun (x : X.Opens) ↦ f ''ᵁ x) U) ((fun (x : X.Opens) ↦ f ''ᵁ x) V)
⊢ U = V

Tactic:
simpa using congrArg (f ⁻¹ᵁ ·) hUV

Premises used: congrArg, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
h : (↑(f ''ᵁ ⨆ (i : ι), s i) : Set ↥Y) = (↑(⨆ (i : ι), f ''ᵁ s i) : Set ↥Y)
⊢ f ''ᵁ ⨆ (i : ι), s i = ⨆ (i : ι), f ''ᵁ s i

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ (↑(f ''ᵁ ⨆ (i : ι), s i) : Set ↥Y) = (↑(⨆ (i : ι), f ''ᵁ s i) : Set ↥Y)

Tactic:
simp [Set.image_iUnion]

Premises used: Set.image_iUnion
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
h : (↑(f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j) : Set ↥Y) = (↑(⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j) : Set ↥Y)
⊢ f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j = ⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
κ : ι → Sort u_2
s : (i : ι) → κ i → X.Opens
⊢ (↑(f ''ᵁ ⨆ (i : ι), ⨆ (j : κ i), s i j) : Set ↥Y) = (↑(⨆ (i : ι), ⨆ (j : κ i), f ''ᵁ s i j) : Set ↥Y)

Tactic:
simp [Set.image_iUnion₂]

Premises used: Set.image_iUnion₂
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : X.Opens
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
⊢ (f ≫ g) ''ᵁ U = g ''ᵁ f ''ᵁ U

Tactic:
TopologicalSpace.Opens.ext (Set.image_comp g f U)

Premises used: CategoryTheory.ConcreteCategory.hom, TopologicalSpace.Opens.ext, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', SetLike.coe, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.image_comp, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : Scheme
U : X.Opens
⊢ 𝟙 X ''ᵁ U = U

Tactic:
TopologicalSpace.Opens.ext (Set.image_id _)

Premises used: TopologicalSpace.Opens.ext, Set.image_id
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
e : X ≅ Y
U : Y.Opens
⊢ e.inv ''ᵁ U = e.hom ⁻¹ᵁ U

Tactic:
TopologicalSpace.Opens.ext <| (Scheme.homeoOfIso e.symm).toEquiv.image_eq_preimage_symm _

Premises used: Homeomorph.toEquiv, AlgebraicGeometry.Scheme.homeoOfIso, TopologicalSpace.Opens.ext, Equiv.image_eq_preimage_symm, CategoryTheory.Iso.symm
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : X.Opens
x : ↥X
⊢ Membership.mem (α := ↥Y) (f ''ᵁ U) (f x : ↥Y) ↔ x ∈ U

Tactic:
f.isOpenEmbedding.injective.mem_set_image

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, Set.Mem, setOf, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, Set.image, Function.Injective.mem_set_image
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ f ⁻¹ᵁ opensRange f = ⊤

Tactic:
simp [Scheme.Hom.opensRange]

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
delta :
  IsIso (X := Γ(Y, (LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
    (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
⊢ IsIso (X := Γ(Y, f ''ᵁ U)) (app f (f ''ᵁ U))

Tactic:
delta opensFunctor

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (X := Γ(Y, (LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
    (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
rw : IsIso (X := Γ(Y, f ''ᵁ f ⁻¹ᵁ V)) (app f (f ''ᵁ f ⁻¹ᵁ V))
⊢ IsIso (app f V)

Tactic:
rw [show V = f ''ᵁ f ⁻¹ᵁ V from Opens.ext (Set.image_preimage_eq_of_subset hV).symm]

Premises used: TopologicalSpace.Opens.ext, Set.image_preimage_eq_of_subset, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
V : Y.Opens
hV : V ≤ opensRange f
⊢ IsIso (X := Γ(Y, f ''ᵁ f ⁻¹ᵁ V)) (app f (f ''ᵁ f ⁻¹ᵁ V))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U V : X.Opens
i : op U ⟶ op V
⊢ X.presheaf.map i ≫ Iso.inv (appIso f V) = Iso.inv (appIso f U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
PresheafedSpace.IsOpenImmersion.inv_naturality _ _

Premises used: Set.Mem, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
rw :
  Eq (α :=
    Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ⟶ X.presheaf.obj (op U))
    (f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫
      X.presheaf.map (eqToHom ⋯))
    (app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯))
⊢ Eq (α :=
    Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ⟶ X.presheaf.obj (op U))
    (f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫
      X.presheaf.map (eqToHom ⋯))
    (app f (f ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rw [eqToHom_op]

Premises used: CategoryTheory.eqToHom_op
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Eq (α :=
    Y.presheaf.obj (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ⟶ X.presheaf.obj (op U))
    (f.toPshHom.c.app (op ((PresheafedSpace.IsOpenImmersion.opensFunctor f.toPshHom).obj U)) ≫
      X.presheaf.map (eqToHom ⋯))
    (app f (f ''ᵁ U) ≫ X.presheaf.map (eqToHom ⋯))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Eq (α := Γ(Y, f ''ᵁ U) ⟶ Γ(X, U)) (Iso.hom (appIso f U)) (appLE f (f ''ᵁ U) U ⋯)

Tactic:
f.appIso_hom U

Premises used: Set.Mem, CategoryTheory.eqToHom, setOf, AlgebraicGeometry.Scheme.Hom.appLE, Set.preimage, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.appIso_hom, Set.image
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ f ⁻¹ᵁ U)) (app f U ≫ Iso.inv (appIso f (f ⁻¹ᵁ U)))
    (Y.presheaf.map
      (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' U.carrier)) (Y := U.carrier)
        (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' U.carrier)) (y := U.carrier) ⋯)))

Tactic:
PresheafedSpace.IsOpenImmersion.app_invApp _ _

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
hU : U ≤ opensRange f
⊢ (↑(f ''ᵁ f ⁻¹ᵁ U) : Set ↥Y) = (↑U : Set ↥Y)

Tactic:
simpa [Set.image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : Y.Opens
hU : U ≤ opensRange f
⊢ app f U ≫ Iso.inv (appIso f (f ⁻¹ᵁ U)) = Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
PresheafedSpace.IsOpenImmersion.app_invApp _ _

Premises used: Eq.mpr, Set.Mem, Quiver.Hom.op, CategoryTheory.eqToHom, setOf, Set.Subset, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp, Set.preimage, Set.image, Set
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
rw rw₁ :
  Eq (α :=
    X.presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toLRSHom f).base) X.presheaf).obj
        (op ((PresheafedSpace.IsOpenImmersion.opensFunctor (toLRSHom f).toHom).obj U)))
    (X.presheaf.map (eqToHom ⋯)) (X.presheaf.map (eqToHom ⋯))
⊢ Eq (α :=
    X.presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward CommRingCat (toLRSHom f).base) X.presheaf).obj
        (op ((PresheafedSpace.IsOpenImmersion.opensFunctor (toLRSHom f).toHom).obj U)))
    (X.presheaf.map (eqToHom ⋯)) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
rw [eqToHom_op]

Premises used: CategoryTheory.eqToHom_op
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
simp :
  Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
    (Y.presheaf.map
        (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
          (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) ⋯)) ≫
      Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V)) (appLE f U V e ≫ Iso.inv (appIso f V)) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [appLE, Category.assoc, appIso_inv_naturality, Functor.op_obj, Functor.op_map,
    Quiver.Hom.unop_op, opensFunctor_map_homOfLE, app_appIso_inv_assoc, Opens.carrier_eq_coe]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE, Quiver.Hom.unop_op, AlgebraicGeometry.Scheme.Hom.app_appIso_inv_assoc, AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality, AlgebraicGeometry.Scheme.Hom.appLE, TopologicalSpace.Opens.carrier_eq_coe, CategoryTheory.Functor.op_obj, CategoryTheory.Functor.op_map
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
rw :
  Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
    (Y.presheaf.map
      (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
          (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) ⋯) ≫
        Quiver.Hom.op (homOfLE ⋯)))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
    (Y.presheaf.map
        (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
          (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) ⋯)) ≫
      Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Eq (α := Γ(Y, U) ⟶ Γ(Y, f ''ᵁ V))
    (Y.presheaf.map
      (Quiver.Hom.op (X := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (Y := (↑U : Set ↥Y))
          (homOfLE (x := Set.image (α := ↥X) (⇑f) (⇑f ⁻¹' (↑U : Set ↥Y))) (y := (↑U : Set ↥Y)) ⋯) ≫
        Quiver.Hom.op (homOfLE ⋯)))
    (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X Y : Scheme
f : X ⟶ Y
inst_1 : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
rwa rwa₁ rwa₂ rwa₃ : ∀ (e : V ≤ U), V ≤ U
⊢ V ≤ U

Tactic:
rwa [preimage_image_eq] at e

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_image_eq
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
simp : X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op
⊢ Iso.inv (appIso f U) ≫ appLE f (f ''ᵁ U) V e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [appLE, appIso_inv_app_assoc, eqToHom_op]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, CategoryTheory.eqToHom_op
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
rw : X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op
⊢ X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
rw :
  X.presheaf.map
      (CategoryStruct.comp (Y := op (f ⁻¹ᵁ f ''ᵁ U)) (Quiver.Hom.op (eqToHom ⋯)) (Quiver.Hom.op (eqToHom ⋯))) =
    X.presheaf.map (𝟙 (op U))
⊢ CategoryStruct.comp (Y := Γ(Y, f ''ᵁ U)) (Iso.inv (appIso f U))
      (app f (f ''ᵁ U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    𝟙 Γ(X, U)

Tactic:
rw [Scheme.Hom.appIso_inv_app_assoc, ← Functor.map_comp, ← X.presheaf.map_id]

Premises used: AlgebraicGeometry.Scheme.Hom.appIso_inv_app_assoc, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map
      (CategoryStruct.comp (Y := op (f ⁻¹ᵁ f ''ᵁ U)) (Quiver.Hom.op (eqToHom ⋯)) (Quiver.Hom.op (eqToHom ⋯))) =
    X.presheaf.map (𝟙 (op U))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ U = 𝟙 X ''ᵁ U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : Scheme
U : X.Opens
w :
  ∀ (x : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)),
    Eq (α := (↑Γ(X, U) : Type u))
      ((CommRingCat.Hom.hom (Iso.hom (appIso (𝟙 X) U)) : (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u)) x :
        (↑Γ(X, U) : Type u))
      ((CommRingCat.Hom.hom (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯))).hom :
            (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u))
          x :
        (↑Γ(X, U) : Type u))
⊢ appIso (𝟙 X) U = Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X : Scheme
U : X.Opens
x : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)
⊢ Eq (α := (↑Γ(X, U) : Type u))
    ((CommRingCat.Hom.hom (Iso.hom (appIso (𝟙 X) U)) : (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u)) x :
      (↑Γ(X, U) : Type u))
    ((CommRingCat.Hom.hom (Functor.mapIso X.presheaf (Iso.op (eqToIso ⋯))).hom :
          (a : (↑Γ(X, 𝟙 X ''ᵁ U) : Type u)) → (↑Γ(X, U) : Type u))
        x :
      (↑Γ(X, U) : Type u))

Tactic:
simp [appIso_hom]

Premises used: AlgebraicGeometry.Scheme.Hom.appIso_hom
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
H : IsOpenImmersion f_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : IsOpenImmersion f
inst_2 : IsOpenImmersion g
U : X.Opens
⊢ g ''ᵁ f ''ᵁ U = (f ≫ g) ''ᵁ U

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
U : X.Opens
w :
  Eq (α := Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U)) (Iso.hom (appIso (f ≫ g) U) : Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))
    (Iso.hom
        (Iso.trans (Y := Z.presheaf.obj (op (g ''ᵁ f ''ᵁ U))) (Functor.mapIso Z.presheaf (Iso.op (eqToIso ⋯)))
          (appIso g (f ''ᵁ U) ≪≫ appIso f U)) :
      Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))
⊢ Eq (α := Γ(Z, (f ≫ g) ''ᵁ U) ≅ Γ(X, U)) (appIso (f ≫ g) U : Γ(Z, (f ≫ g) ''ᵁ U) ≅ Γ(X, U))
    (Iso.trans (Y := Z.presheaf.obj (op (g ''ᵁ f ''ᵁ U))) (Functor.mapIso Z.presheaf (Iso.op (eqToIso ⋯)))
        (appIso g (f ''ᵁ U) ≪≫ appIso f U) :
      Z.presheaf.obj (op ((f ≫ g) ''ᵁ U)) ≅ Γ(X, U))

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
inst_1 : IsOpenImmersion g
U : X.Opens
⊢ Eq (α := Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U)) (Iso.hom (appIso (f ≫ g) U) : Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))
    (Iso.hom
        (Iso.trans (Y := Z.presheaf.obj (op (g ''ᵁ f ''ᵁ U))) (Functor.mapIso Z.presheaf (Iso.op (eqToIso ⋯)))
          (appIso g (f ''ᵁ U) ≪≫ appIso f U)) :
      Γ(Z, (f ≫ g) ''ᵁ U) ⟶ Γ(X, U))

Tactic:
simp [appIso_hom, app_eq_appLE, appLE_comp_appLE, -comp_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appIso_hom, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
apply :
  IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
apply₁ :
  IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
            (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base
              (InducedCategory.Hom.hom
                (LocallyRingedSpace.Hom.toShHom
                  (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
        (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u)))) →
    ∀ (x : ↥(Spec (CommRingCat.of (Localization.Away f)))),
      IsIso (X :=
        (Spec (CommRingCat.of (↑R : Type u))).presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
                (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
                (PresheafedSpace.Hom.base
                  (InducedCategory.Hom.hom
                    (LocallyRingedSpace.Hom.toShHom
                      (Hom.toLRSHom
                        (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))) :
              (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))
            x))
        (PresheafedSpace.Hom.stalkMap
          (InducedCategory.Hom.hom
            (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f)))))))
          x)
⊢ IsOpenImmersion.{u} (X := Spec (CommRingCat.of (Localization.Away f))) (Y := Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))

Tactic:
apply SheafedSpace.IsOpenImmersion.of_stalk_iso (H := ?_)

Premises used: AlgebraicGeometry.SheafedSpace.IsOpenImmersion.of_stalk_iso
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
⊢ IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))

Tactic:
(PrimeSpectrum.localization_away_isOpenEmbedding (Localization.Away f) f :)

Premises used: PrimeSpectrum.localization_away_isOpenEmbedding, Set.Mem, OreLocalization, setOf, Localization.Away, Quotient, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
R : CommRingCat
f : (↑R : Type u)
⊢ IsOpenEmbedding (X := ↥(Spec (CommRingCat.of (Localization.Away f)))) (Y := ↥(Spec (CommRingCat.of (↑R : Type u))))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(Spec (CommRingCat.of (Localization.Away f))).toPresheafedSpace : TopCat)) (Y :=
          (↑(Spec (CommRingCat.of (↑R : Type u))).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base
            (InducedCategory.Hom.hom
              (LocallyRingedSpace.Hom.toShHom
                (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away f))))))))) :
      (a : ↥(Spec (CommRingCat.of (Localization.Away f)))) → ↥(Spec (CommRingCat.of (↑R : Type u))))

Tactic:
exact (PrimeSpectrum.localization_away_isOpenEmbedding (Localization.Away f) f :)

Premises used: PrimeSpectrum.localization_away_isOpenEmbedding, Localization.Away