awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))

Tactic:
have : (toNormalization f).appLE (f₁ ⁻¹ᵁ g ⁻¹ᵁ U.val) (f ⁻¹ᵁ U.val) h₁ =
        f.normalization.presheaf.map (eqToHom h₂).op ≫
        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.val) ≫
          X.presheaf.map (eqToHom h₃).op := by
        simp [app_eq_appLE]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
rw :
  Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    Spec.map
        ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
          (Iso.hom (normalizationObjIso f ⋯) ≫
              CommRingCat.ofHom
                  (↑(Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
                      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
                X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
            X.presheaf.map (Quiver.Hom.op (eqToHom h₃))) ≫
      ⋯.fromSpec ≫ f₁
⊢ Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    Spec.map (appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec ≫ f₁

Tactic:
rw [this, f.toNormalization_app_preimage U]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂)) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
⊢ Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₁ =
    CategoryStruct.comp (Y :=
      Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
      (Spec.map
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
          𝟙 Γ(X, f ⁻¹ᵁ (↑U : Y.Opens))))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯) ≫
        f₁)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
simp :
  Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫
      Spec.map (appLE f₂ (g ⁻¹ᵁ (↑U : Y.Opens)) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
⊢ Spec.map (appLE f₀ (g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) h₁) ≫ ⋯.fromSpec =
    Spec.map
        (CommRingCat.ofHom
          (AlgHom.toRingHom
            (Subalgebra.val
              (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
simp only [AlgHom.toRingHom_eq_coe, hf₀, comp_appLE, Spec.map_comp, Category.assoc,
        app_eq_appLE]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_appLE, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgHom.toRingHom_eq_coe, AlgebraicGeometry.Spec.map_comp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
rw :
  Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫
      Spec.map (appLE f₂ (g ⁻¹ᵁ (↑U : Y.Opens)) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
rw [IsAffineOpen.SpecMap_appLE_fromSpec _ _ ((U.2.preimage _).preimage _)]

Premises used: AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))

Tactic:
simp [app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
⊢ appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))

Tactic:
have : (toNormalization f).appLE (f₂ ⁻¹ᵁ g ⁻¹ᵁ U.1) (f ⁻¹ᵁ U.1) h₁'.le =
        f.normalization.presheaf.map (eqToHom h₂').op ≫
        (toNormalization f).app (f.fromNormalization ⁻¹ᵁ U.1) ≫
          X.presheaf.map (eqToHom h₃).op := by
        simp [app_eq_appLE]
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
rw :
  Spec.map
        ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
          (Iso.hom (normalizationObjIso f ⋯) ≫
              CommRingCat.ofHom
                  (↑(Subalgebra.val
                        (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
                    ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
                      (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
                X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
            X.presheaf.map (Quiver.Hom.op (eqToHom h₃))) ≫
      ⋯.fromSpec ≫ f₂ =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
⊢ Spec.map (appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯) ≫ ⋯.fromSpec ≫ f₂ =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
rw [this, f.toNormalization_app_preimage U]

Premises used: AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
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 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
⊢ CategoryStruct.comp (Y :=
      Spec (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
      (Spec.map
        (CommRingCat.ofHom
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
          𝟙 Γ(X, f ⁻¹ᵁ (↑U : Y.Opens))))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯) ≫
        f₂) =
    Spec.map
        (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ iU ≫ f = CategoryStruct.comp (Y := normalization f) (iU ≫ toNormalization f) (fromNormalization f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
⊢ iV ≫ f = CategoryStruct.comp (Y := normalization f) (iV ≫ toNormalization f) (fromNormalization f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
simp :
  Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ Y)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
⊢ f =
    CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
        (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)))

Tactic:
simp only [← Iso.inv_comp_eq, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_comp_eq