awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ appLE f U (f ⁻¹ᵁ U) ⋯ = app f U

Tactic:
(app_eq_appLE f).symm

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : {R S : CommRingCat.{u}} → (R ⟶ S) → Prop
subst : P (appLE f U V e) ↔ P (appLE f U V' ⋯)
⊢ P (appLE f U V e) ↔ P (appLE f U' V' ⋯)

Tactic:
subst e₁
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₂ : V = V'
P : {R S : CommRingCat.{u}} → (R ⟶ S) → Prop
subst : P (appLE f U V e) ↔ P (appLE f U V ⋯)
⊢ P (appLE f U V e) ↔ P (appLE f U V' ⋯)

Tactic:
subst e₂
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
P : {R S : CommRingCat.{u}} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U V ⋯)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) = app g U
mk :
  ∀ (toLRSHom' : X.Hom Y.toLocallyRingedSpace) (h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = g.base)
    (h_app :
      ∀ (U : Y.Opens),
        { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) = app g U),
    { toLRSHom' := toLRSHom' : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
g : X ⟶ Y
toLRSHom' : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = g.base
h_app :
  ∀ (U : Y.Opens), { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) = app g U
mk :
  ∀ (toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace)
    (h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base)
    (h_app :
      ∀ (U : Y.Opens),
        { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
          { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U),
    { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = g

Tactic:
cases g
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
mk : toLRSHom' = toLRSHom'_1
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
mk : toLRSHom'.toHom = toLRSHom'_1.toHom
⊢ toLRSHom' = toLRSHom'_1

Tactic:
apply LocallyRingedSpace.Hom.ext'

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.ext'
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
mk : toLRSHom'.base = toLRSHom'_1.base
mk₁ : toLRSHom'.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'_1.c
⊢ toLRSHom'.toHom = toLRSHom'_1.toHom

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ toLRSHom'.base = toLRSHom'_1.base

Tactic:
h_base
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ toLRSHom'.base = toLRSHom'_1.base

Tactic:
exact h_base
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
U : TopologicalSpace.Opens ↥Y
⊢ Eq (α := Y.presheaf.obj (op U) ⟶ ((Opens.map toLRSHom'_1.base).op ⋙ X.presheaf).obj (op U))
    ((toLRSHom'.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op U)) (toLRSHom'_1.c.app (op U))

Tactic:
simpa using h_app U
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom' : X.Hom Y }.base = { toLRSHom' := toLRSHom'_1 }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom' : X.Hom Y }.app U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
      { toLRSHom' := toLRSHom'_1 : X.Hom Y }.app U
⊢ toLRSHom'.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'_1.c

Tactic:
exact TopCat.Presheaf.ext (fun U ↦ by simpa using h_app U)

Premises used: TopCat.Presheaf.ext
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
mk :
  ∀ (toLRSHom' : X.Hom Y.toLocallyRingedSpace) (h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = toLRSHom g),
    { toLRSHom' := toLRSHom' : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
g : X ⟶ Y
toLRSHom' : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = toLRSHom g
mk :
  ∀ (toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace)
    (h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = { toLRSHom' := toLRSHom'_1 }.toLRSHom),
    { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = g

Tactic:
cases g
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
toLRSHom' toLRSHom'_1 : X.Hom Y.toLocallyRingedSpace
h : { toLRSHom' := toLRSHom' : X.Hom Y }.toLRSHom = { toLRSHom' := toLRSHom'_1 }.toLRSHom
⊢ { toLRSHom' := toLRSHom' : X.Hom Y } = { toLRSHom' := toLRSHom'_1 }

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
⊢ x ∈ f ⁻¹ᵁ U ↔ Membership.mem (α := ↥Y) U (f x : ↥Y)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (↑(f ⁻¹ᵁ U) : Set ↥X) = ⇑f ⁻¹' (↑U : Set ↥Y)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
⊢ f ⁻¹ᵁ (U ⊔ V) = f ⁻¹ᵁ U ⊔ f ⁻¹ᵁ V

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
⊢ f ⁻¹ᵁ (U ⊓ V) = f ⁻¹ᵁ U ⊓ f ⁻¹ᵁ V

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ f ⁻¹ᵁ ⊤ = ⊤

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ f ⁻¹ᵁ ⊥ = ⊥

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
⊢ (↑(f ⁻¹ᵁ iSup U) : Set ↥X) = (↑(⨆ (i : ι), f ⁻¹ᵁ U i) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
hU : iSup U = ⊤
⊢ Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), f ⁻¹ᵁ U i) ⊤

Tactic:
f.preimage_iSup U ▸ hU ▸ rfl

Premises used: AlgebraicGeometry.Scheme.Hom.preimage_iSup, Eq.rec, Eq.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
hUU' : U ≤ U'
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ U'

Tactic:
fun _ ha ↦ hUU' ha

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
⊢ (f ≫ g) ⁻¹ᵁ U = f ⁻¹ᵁ g ⁻¹ᵁ U

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
⊢ forgetToLocallyRingedSpace.Full

Tactic:
fullyFaithfulForgetToLocallyRingedSpace.full

Premises used: AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace, CategoryTheory.Functor.FullyFaithful.full
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
⊢ forgetToLocallyRingedSpace.Faithful

Tactic:
fullyFaithfulForgetToLocallyRingedSpace.faithful

Premises used: AlgebraicGeometry.Scheme.fullyFaithfulForgetToLocallyRingedSpace, CategoryTheory.Functor.FullyFaithful.faithful
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
⊢ Eq (α := (a : ↥X) → ↥Y) (⇑(homeoOfIso e) : (a : ↥X) → ↥Y) ⇑e.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
⊢ Eq (α := (a : ↥Y) → ↥X) (⇑(homeoOfIso e.symm) : (a : ↥Y) → ↥X) ⇑e.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
⊢ (homeoOfIso e).symm = homeoOfIso e.symm

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.homeoOfIso, TopCat.homeoOfIso, Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ Eq (α := ↥Y) ((homeoOfIso e : (a : ↥X) → ↥Y) x : ↥Y) (e.hom x : ↥Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
x : ↥X
⊢ Eq (α := ↥Y) ((homeomorph f : (a : ↥X) → ↥Y) x : ↥Y) (f x : ↥Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
⊢ forgetToTop ⋙
      CategoryTheory.forget TopCat (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
        carrier) =
    forget

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.forget, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
⊢ forget.obj X = ↥X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Eq (α := (a : (fun (X : Type u_1) ↦ X) (forget.obj X)) → (fun (X : Type u_1) ↦ X) (forget.obj Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map f)) :
      (a : (fun (X : Type u_1) ↦ X) (forget.obj X)) → (fun (X : Type u_1) ↦ X) (forget.obj Y))
    ⇑f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ forget.map f = ↾⇑f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
⊢ (toLRSHom' (𝟙 X)).base = 𝟙 (↑X.toPresheafedSpace : TopCat)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ app (𝟙 X) U = 𝟙 Γ(X, U)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
⊢ appTop (𝟙 X) = 𝟙 Γ(X, ⊤)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ toLRSHom (f ≫ g) = toLRSHom f ≫ toLRSHom g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (f ≫ g).base = f.base ≫ g.base

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
⊢ Eq (α := ↥Z) ((f ≫ g) x : ↥Z) (g (f x : ↥Y) : ↥Z)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
⊢ app (f ≫ g) U = app g U ≫ app f (g ⁻¹ᵁ U)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ appTop (f ≫ g) = appTop g ≫ appTop f

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
dsimp :
  (app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
⊢ appLE g U V e₁ ≫ appLE f V W e₂ = appLE (f ≫ g) U W ⋯

Tactic:
dsimp [Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
rw :
  app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op
⊢ (app g U ≫ Y.presheaf.map (homOfLE e₁).op) ≫ app f V ≫ X.presheaf.map (homOfLE e₂).op =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [Category.assoc, f.naturality_assoc, ← Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.naturality_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ app g U ≫ app f (g ⁻¹ᵁ U) ≫ X.presheaf.map (((Opens.map f.base).map (homOfLE e₁).op.unop).op ≫ (homOfLE e₂).op) =
    (app g U ≫ app f (g ⁻¹ᵁ U)) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
rw : appLE (f ≫ g) U V e = appLE g U (g ⁻¹ᵁ U) ⋯ ≫ appLE f (g ⁻¹ᵁ U) V e
rw₁ rw₂ : appLE (f ≫ g) U V e = appLE (f ≫ g) U V ⋯
⊢ appLE (f ≫ g) U V e = app g U ≫ appLE f (g ⁻¹ᵁ U) V e

Tactic:
rw [g.app_eq_appLE, appLE_comp_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
subst : f ⁻¹ᵁ U = f ⁻¹ᵁ U
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ f ⁻¹ᵁ U = f ⁻¹ᵁ U

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
subst : app f U = app f U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ app f U = app g U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = app f U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ app f U = Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ app f V ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X = Y
U : Y.Opens
subst : ∀ (U : X.Opens), Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ Γ(X, U) = Γ(X, eqToHom ⋯ ⁻¹ᵁ U)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X = Y
U : Y.Opens
subst : ∀ (U : X.Opens), app (eqToHom ⋯) U = eqToHom ⋯
⊢ app (eqToHom e) U = eqToHom ⋯

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
⊢ app (eqToHom ⋯) U = eqToHom ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ IsIso (toLRSHom f)

Tactic:
forgetToLocallyRingedSpace.map_isIso f

Premises used: CategoryTheory.Functor.map_isIso, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ IsIso f.toPshHom

Tactic:
inferInstanceAs (IsIso ((LocallyRingedSpace.forgetToSheafedSpace ⋙
    SheafedSpace.forgetToPresheafedSpace).map f.toLRSHom))

Premises used: _private.0.AlgebraicGeometry.Scheme.Hom.isIso_toPshHom._proof_1
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ IsIso f.base

Tactic:
Scheme.forgetToTop.map_isIso f

Premises used: AlgebraicGeometry.Scheme.forgetToTop, CategoryTheory.Functor.map_isIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Y.Opens
⊢ IsIso (app f U)

Tactic:
haveI := PresheafedSpace.c_isIso_of_iso f.toPshHom
  NatIso.isIso_app_of_isIso f.c _

Premises used: CategoryTheory.NatIso.isIso_app_of_isIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Opposite.op, AlgebraicGeometry.PresheafedSpace.Hom.c
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : 𝟙 X ⁻¹ᵁ U = U
⊢ (f ≫ inv f) ⁻¹ᵁ U = U

Tactic:
rw [IsIso.hom_inv_id]

Premises used: CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
⊢ 𝟙 X ⁻¹ᵁ U = U

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : X.Opens
rw : app (inv f) U ≫ app f (inv f ⁻¹ᵁ U) = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₁ : app (f ≫ inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
rw₂ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (app (𝟙 X) U ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₃ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (𝟙 Γ(X, U) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
rw₄ rw₅ :
  Eq (α := Γ(X, U) ⟶ Γ(X, (f ≫ inv f) ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ app (inv f) U = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ inv (app f (inv f ⁻¹ᵁ U))

Tactic:
rw [IsIso.eq_comp_inv, ← comp_app, congr_app (IsIso.hom_inv_id f), id_app, Category.id_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.Scheme.Hom.id_app, CategoryTheory.IsIso.eq_comp_inv, CategoryTheory.IsIso.hom_inv_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
⊢ appTop (inv f) = inv (appTop f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
subst : f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }
⊢ f.base = ofHom { toFun := g, continuous_toFun := ⋯ }

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
⊢ f.base = ofHom { toFun := ⇑f, continuous_toFun := ⋯ }

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
subst :
  IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom { toFun := ⇑f, continuous_toFun := ⋯ }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := ⇑f, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))
⊢ IsLocalHom (R :=
    (↑(Y.presheaf.stalk
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                (ofHom { toFun := g, continuous_toFun := ⋯ }) :
              (a : ↥X) → ↥Y)
            x)) :
      Type u_1))
    (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X := (↑X.toPresheafedSpace : TopCat)) (Y := (↑Y.toPresheafedSpace : TopCat))
                  (ofHom { toFun := g, continuous_toFun := ⋯ }) :
                (a : ↥X) → ↥Y)
              x)) :
        Type u_1) →+*
      (↑(X.presheaf.stalk x) : Type u_1))
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
subst h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X.Hom Y
x : ↥X
⊢ IsLocalHom (R := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (S := (↑(X.presheaf.stalk x) : Type u_1)) (F :=
    (↑(Y.presheaf.stalk (f x)) : Type u_1) →+* (↑(X.presheaf.stalk x) : Type u_1)) (CommRingCat.Hom.hom (f.stalkMap x))

Tactic:
f.prop x

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.Hom.prop