awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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
⊢ 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)))
have simp : CommRingCat.Hom.hom (appLE f V (f ⁻¹ᵁ U) sorry) =
  CommRingCat.Hom.hom (f.c.app (Opposite.op V) ≫ X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op)
Tactic: simp [RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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
⊢ 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))
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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)
⊢ 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))
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opensᵒᵖ
⊢ 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)))
have 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)) sorry) =
  𝟙 (CommRingCat.of ↥(integralClosure (↑(Y.presheaf.obj U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)))
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U V : (TopologicalSpace.Opens ↥Y)ᵒᵖ
i : U ⟶ V
⊢ 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
have 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))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
⊢ NatTrans.Coequifibered ((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f))
have refine : ∀ (U : Y.AffineZariskiSite) (r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)),
  IsLocalization.Away (R := (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U))
            (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
        r :
      (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r))) : Type u)
Tactic: refine coequifibered_iff_forall_isLocalizationAway.mpr fun U r ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
⊢ IsLocalization.Away (R := (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U))
            (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
        r :
      (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r))) : Type u)
have this₁ : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
Tactic: have : IsLocalization.Away r Γ(Y, Y.basicOpen r) :=
    U.2.isLocalization_basicOpen _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
⊢ IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
have rw! : IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      r :
    (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ (↑U : Y.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, (↑U : Y.Opens))) (app f (↑U : Y.Opens)) :
              (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            r)) :
    Type u)
Tactic: rw! (castMode := .all) [f.preimage_basicOpen r]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U))
            (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
        r :
      (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r))) : Type u)
have this₁ : IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
      r :
    (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
Tactic: have : IsLocalization.Away ((algebraMap ↑Γ(Y, U.1) ↑Γ(X, f ⁻¹ᵁ U.1)) r)
      Γ(X, f ⁻¹ᵁ Y.basicOpen r) := by
    let : Algebra Γ(X, f ⁻¹ᵁ U.1) Γ(X, X.basicOpen (f.app _ r)) :=
      (X.presheaf.map (homOfLE (X.basicOpen_le _)).op).hom.toAlgebra
    dsimp +instances [inst]
    rw! (castMode := .all) [f.preimage_basicOpen r]
    exact isLocalization_basicOpen_of_qcqs (f.isCompact_preimage U.2.isCompact)
        (f.isQuasiSeparated_preimage U.2.isQuasiSeparated) (f.app _ r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := ((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U))
            (((toOpensFunctor Y).op.whiskerLeft (normalizationDiagramMap f)).app (Opposite.op U)) :
          (a : (↑(((toOpensFunctor Y).op ⋙ Y.presheaf).obj (Opposite.op U)) : Type u)) →
            (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
        r :
      (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op U)) : Type u))
    (↑(((toOpensFunctor Y).op ⋙ normalizationDiagram f).obj (Opposite.op (U.basicOpen r))) : Type u)
have change : IsLocalization.Away (R := ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
  ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u)
          ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
        (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
          ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
      r :
    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
Tactic: change IsLocalization.Away ((algebraMap Γ(Y, U.1) (integralClosure Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1))) r)
    (integralClosure Γ(Y, Y.basicOpen r) Γ(X, f ⁻¹ᵁ Y.basicOpen r))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : QuasiCompact f
inst_2 : QuasiSeparated f
U : Y.AffineZariskiSite
r : (↑Γ(Y, (↑U : Y.Opens)) : Type u)
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : Algebra (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑(U.basicOpen r) : Y.Opens)))
this_3 : Algebra ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
  ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)) :=
  (CommRingCat.Hom.hom ((normalizationDiagram f).map (homOfLE ⋯).op)).toAlgebra
inst : Algebra (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).toAlgebra
this_4 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this_5 :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) → (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
    (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
this : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u) :=
  (CommRingCat.Hom.hom (appLE f (↑U : Y.Opens) (f ⁻¹ᵁ Y.basicOpen r) ⋯)).toAlgebra
⊢ IsLocalization.Away (R := ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ((algebraMap (↑Γ(Y, (↑U : Y.Opens)) : Type u)
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) :
          (a : (↑Γ(Y, (↑U : Y.Opens)) : Type u)) →
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
        r :
      ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
    ↥(integralClosure (↑Γ(Y, Y.basicOpen r) : Type u) (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
have this₁ : IsScalarTower.{u, u, u} (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)
  (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u)
Tactic: have : IsScalarTower Γ(Y, U.1) Γ(X, f ⁻¹ᵁ U.1) Γ(X, f ⁻¹ᵁ Y.basicOpen r) := .of_algebraMap_eq' rfl