awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ (↑⊤ : Set ↥X)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2) : ↥X)) : Type u_1)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2)).asIdeal
⊢ IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
exact @IsLocalization.isNoetherianRing _ _ (hU.primeIdealOf ⟨x, hU2⟩).asIdeal.primeCompl
        (X.presheaf.stalk x) _ (X.presheaf.algebra_section_stalk ⟨x, hU2⟩)
        this (IsLocallyNoetherian.component_noetherian ⟨U, hU⟩)

Premises used: CommRingCat.carrier, IsLocalization.isNoetherianRing, TopCat.Presheaf.stalk, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Ideal.primeCompl, PrimeSpectrum.asIdeal, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : CommRingCat
⊢ IsNoetherian.{u_1} (Spec R) ↔ IsNoetherianRing.{u_1} (↑R : Type u_1)

Tactic:
simp [AlgebraicGeometry.isNoetherian_iff, (inferInstance : CompactSpace (Spec R))]

Premises used: AlgebraicGeometry.isNoetherian_iff, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
⊢ Set.Finite.{u_1} (α := Set ↥X) (irreducibleComponents ↥X)

Tactic:
NoetherianSpace.finite_irreducibleComponents

Premises used: TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
V U : Y.Opensᵒᵖ
i : V ⟶ U
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)
hx :
  Membership.mem (γ := Subalgebra (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) x
obtain :
  ∀ (U : Y.Opens) (i : V ⟶ Opposite.op U),
    Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
      Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
      (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))

Tactic:
obtain ⟨U, rfl⟩ := Opposite.op_surjective U

Premises used: rfl, Opposite.op_surjective
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
V : Y.Opensᵒᵖ
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)
hx :
  Membership.mem (γ := Subalgebra (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) x
U : Y.Opens
i : V ⟶ Opposite.op U
obtain :
  ∀ (V : Y.Opens) (x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (hx :
      Membership.mem (γ :=
        Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
          (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
        (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
          (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
        x)
    (i : Opposite.op V ⟶ Opposite.op U),
    Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
      Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
      (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
            (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)) →
              (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
          x :
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))

Tactic:
obtain ⟨V, rfl⟩ := Opposite.op_surjective V

Premises used: rfl, Opposite.op_surjective
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
simp :
  CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯) =
    CommRingCat.Hom.hom (f.c.app (Opposite.op V) ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)
⊢ Eq.{u + 1} (α := (↑Γ(Y, V) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (algebraMap (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (@RingHom.comp _ (↑Γ(Y, U) : Type u) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) (algebraMap (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u)))

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp]

Premises used: CommRingCat.hom_comp, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯) =
    CommRingCat.Hom.hom (f.c.app (Opposite.op V) ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
⊢ IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)

Tactic:
have : IsScalarTower Γ(Y, V) Γ(Y, U) Γ(X, f ⁻¹ᵁ U) := .of_algebraMap_eq' <| by
        simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp]; rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
this : IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)
⊢ IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)

Tactic:
have : IsScalarTower Γ(Y, V) Γ(X, f ⁻¹ᵁ V) Γ(X, f ⁻¹ᵁ U) := .of_algebraMap_eq' rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
this_1 : IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)
this : IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)) →
            (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))

Tactic:
(hx.map (IsScalarTower.toAlgHom Γ(Y, V) _ Γ(X, f ⁻¹ᵁ U))).tower_top

Premises used: CommRingCat.carrier, Set.Mem, setOf, IsScalarTower.toAlgHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', RingHom.IsIntegralElem, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsIntegral, IsIntegral.map, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, IsIntegral.tower_top, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
hx :
  Membership.mem (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
    x
i : Opposite.op V ⟶ Opposite.op U
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) := (CommRingCat.Hom.hom (app f V)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) := (CommRingCat.Hom.hom (Y.presheaf.map i)).toAlgebra
algInst_3 : Algebra (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
algInst_4 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) :=
  (CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) ⋯)).toAlgebra
this_1 : IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)
this : IsScalarTower.{u, u, u} (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)) →
            (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))

Tactic:
exact (hx.map (IsScalarTower.toAlgHom Γ(Y, V) _ Γ(X, f ⁻¹ᵁ U))).tower_top

Premises used: CommRingCat.carrier, IsScalarTower.toAlgHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, IsIntegral.map, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, IsIntegral.tower_top, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opensᵒᵖ
simp :
  CommRingCat.ofHom
      (RingHom.restrict (RingHom.id (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        (integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        (integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)) ⋯) =
    𝟙 (CommRingCat.of ↥(integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)))
⊢ CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
        (integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        (integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)) ⋯) =
    𝟙 (CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opensᵒᵖ
⊢ CommRingCat.ofHom
      (RingHom.restrict (RingHom.id (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        (integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        (integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)) ⋯) =
    𝟙 (CommRingCat.of ↥(integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
X_1 Y_1 Z : Y.Opensᵒᵖ
i : X_1 ⟶ Y_1
j : Y_1 ⟶ Z
⊢ Eq.{u + 1} (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
    (CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op)).restrict
        (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
        (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯))
    (CommRingCat.ofHom
      (@RingHom.comp _ ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
        _ _ Semiring.toNonAssocSemiring _
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
            (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
            (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯ :
          ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) →+*
            ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
          (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
          (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) ⋯)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
hf :
  ∀ (x : (↑(Y.presheaf.obj U) : Type u)),
    Eq (α := (↑((normalizationDiagram f).obj V) : Type u))
      ((CommRingCat.Hom.hom
              (Y.presheaf.map i ≫
                CommRingCat.ofHom
                  (algebraMap (↑Γ(Y, Opposite.unop V) : Type u)
                    ↥(integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)))) :
            (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
          x :
        (↑((normalizationDiagram f).obj V) : Type u))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                  (algebraMap (↑Γ(Y, Opposite.unop U) : Type u)
                    ↥(integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))) ≫
                (normalizationDiagram f).map i) :
            (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
          x :
        (↑((normalizationDiagram f).obj V) : Type u))
⊢ Y.presheaf.map i ≫
      CommRingCat.ofHom
        (algebraMap (↑Γ(Y, Opposite.unop V) : Type u)
          ↥(integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u))) =
    CommRingCat.ofHom
        (algebraMap (↑Γ(Y, Opposite.unop U) : Type u)
          ↥(integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))) ≫
      (normalizationDiagram f).map i

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
x : (↑(Y.presheaf.obj U) : Type u)
⊢ Eq (α := (↑((normalizationDiagram f).obj V) : Type u))
    ((CommRingCat.Hom.hom
            (Y.presheaf.map i ≫
              CommRingCat.ofHom
                (algebraMap (↑Γ(Y, Opposite.unop V) : Type u)
                  ↥(integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)))) :
          (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
        x :
      (↑((normalizationDiagram f).obj V) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                (algebraMap (↑Γ(Y, Opposite.unop U) : Type u)
                  ↥(integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))) ≫
              (normalizationDiagram f).map i) :
          (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
        x :
      (↑((normalizationDiagram f).obj V) : Type u))

Tactic:
Subtype.ext congr($(f.naturality i) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgebraicGeometry.Scheme.Hom.naturality, DFunLike.coe, Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
x : (↑(Y.presheaf.obj U) : Type u)
⊢ Eq (α := (↑((normalizationDiagram f).obj V) : Type u))
    ((CommRingCat.Hom.hom
            (Y.presheaf.map i ≫
              CommRingCat.ofHom
                (algebraMap (↑Γ(Y, Opposite.unop V) : Type u)
                  ↥(integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)))) :
          (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
        x :
      (↑((normalizationDiagram f).obj V) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                (algebraMap (↑Γ(Y, Opposite.unop U) : Type u)
                  ↥(integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))) ≫
              (normalizationDiagram f).map i) :
          (a : (↑(Y.presheaf.obj U) : Type u)) → (↑((normalizationDiagram f).obj V) : Type u))
        x :
      (↑((normalizationDiagram f).obj V) : Type u))

Tactic:
exact Subtype.ext congr($(f.naturality i) x)
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ NatTrans.Coequifibered ((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))

Tactic:
coequifibered_iff_forall_isLocalizationAway.mpr fun U r ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.Scheme.AffineZariskiSite.coequifibered_iff_forall_isLocalizationAway