Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝¹ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  (CommRingCat.Hom.hom (app (pullback.snd f g) V)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  ⋯.isoPushout ≪≫ pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯)
e : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U) ≃ₐ[↑Γ(Y, V)] ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  let __RingEquiv := e₀.commRingCatIsoToRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
ψ : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)) →ₐ[↑Γ(Y, V)]
  ↥(integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) :=
  (↑e.mapIntegralClosure).comp (toIntegralClosure ↑Γ(S, U) ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U))
hψ : Function.Bijective ⇑ψ
φ : pushout (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) :=
  pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
      (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))) (appLE g U V hVU)
      (normalizationObjIso f hU).hom (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯ ≫
    ⋯.isoPushout.inv ≫
      (RingEquiv.ofBijective ψ.toRingHom hψ).toCommRingCatIso.hom ≫
        (normalizationObjIso (pullback.snd f g) hV).inv ≫ (normalization (pullback.snd f g)).presheaf.map (eqToHom ⋯).op
⊢ pushout.inr (app (fromNormalization f) U) (appLE g U V hVU) ≫
      pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
          (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU)
          (𝟙 Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯ ≫
        pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W =
    pushout.inr (app (fromNormalization f) U) (appLE g U V hVU) ≫
      pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
          (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))) (appLE g U V hVU)
          (normalizationObjIso f hU).hom (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯ ≫
        ⋯.isoPushout.inv ≫
          CommRingCat.ofHom ↑(RingEquiv.ofBijective (↑ψ) hψ) ≫
            (normalizationObjIso (pullback.snd f g) hV).inv ≫
              (normalization (pullback.snd f g)).presheaf.map (eqToHom ⋯).op

Tactic:
simp only [Scheme.Hom.app_eq_appLE, colimit.ι_desc_assoc, span_right, PushoutCocone.mk_pt,
      PushoutCocone.mk_ι_app, Category.id_comp, Scheme.Hom.appLE_comp_appLE,
      Scheme.Hom.normalizationPullback_snd, eqToHom_op, IsPushout.inr_isoPushout_inv_assoc]

Goal state after:
case h₁
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝⁴ : QuasiCompact f✝
inst✝³ : QuasiSeparated f✝
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : QuasiCompact f
inst✝¹ : QuasiSeparated f
inst✝ : Smooth g
x : ↥(pullback (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : (pullback.snd (fromNormalization f) g ≫ g) x ∈ ↑U
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : (pullback.snd (fromNormalization f) g) x ∈ ↑V
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this✝¹ : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
this✝ : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst✝² : Algebra ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst✝¹ : Algebra ↑Γ(S, U) ↑Γ(Y, V) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst✝ : Algebra ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  (CommRingCat.Hom.hom (app (pullback.snd f g) V)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(S, U) ↑Γ(Y, V)
this : IsIso (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    (↑(Y.presheaf.1 (Opposite.op V)) ⊗[↑(S.presheaf.1 (Opposite.op U))] ↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U)))) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  ⋯.isoPushout ≪≫ pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯)
e : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↑Γ(X, f ⁻¹ᵁ U) ≃ₐ[↑Γ(Y, V)] ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  let __RingEquiv := e₀.commRingCatIsoToRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
ψ : ↑Γ(Y, V) ⊗[↑Γ(S, U)] ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)) →ₐ[↑Γ(Y, V)]
  ↥(integralClosure ↑Γ(Y, V) ↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) :=
  (↑e.mapIntegralClosure).comp (toIntegralClosure ↑Γ(S, U) ↑Γ(Y, V) ↑Γ(X, f ⁻¹ᵁ U))
hψ : Function.Bijective ⇑ψ
φ : pushout (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) :=
  pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
      (CommRingCat.ofHom (algebraMap ↑Γ(S, U) ↥(integralClosure ↑Γ(S, U) ↑Γ(X, f ⁻¹ᵁ U)))) (appLE g U V hVU)
      (normalizationObjIso f hU).hom (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯ ≫
    ⋯.isoPushout.inv ≫
      (RingEquiv.ofBijective ψ.toRingHom hψ).toCommRingCatIso.hom ≫
        (normalizationObjIso (pullback.snd f g) hV).inv ≫ (normalization (pullback.snd f g)).presheaf.map (eqToHom ⋯).op
⊢ appLE (fromNormalization (pullback.snd f g)) V (normalizationPullback f g ⁻¹ᵁ W) ⋯ =
    CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫
      CommRingCat.ofHom ↑(RingEquiv.ofBijective (↑ψ) hψ) ≫
        (normalizationObjIso (pullback.snd f g) hV).inv ≫ (normalization (pullback.snd f g)).presheaf.map (eqToHom ⋯)