awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
refine_1 : IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
refine_2 :
  ∀ (x : (↑Γ(X, V) : Type u)),
    Eq (α := (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
          ((ψ₁ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
        (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
          ((ψ₂ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
        (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
⊢ ψ₁ = ψ₂

Tactic:
refine Algebra.FormallyUnramified.ext' (i.app W).hom ?_ ψ₁ ψ₂ ?_

Premises used: CommRingCat.Hom.hom, Algebra.FormallyUnramified.ext', AlgebraicGeometry.Scheme.Hom.app
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
refine_1 :
  ∀ (n : ℕ) (hn : Scheme.Hom.ker i ^ n = 0),
    IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))
⊢ IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))

Tactic:
obtain ⟨n, hn⟩ := hi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ IsNilpotent (R := Ideal (↑Γ(Z, W) : Type u)) (RingHom.ker (CommRingCat.Hom.hom (Scheme.Hom.app i W)))

Tactic:
exact ⟨n, by simpa using congr(($hn).ideal ⟨W, hW⟩)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst : IsClosedImmersion i
f : X ⟶ Y
inst_1 : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this_1 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
this_2 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algInst_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE (g₁ ≫ f) U W ⋯)).toAlgebra
algebraizeInst : Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
ψ₁ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯), commutes' := ⋯ }
ψ₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] (↑Γ(Z, W) : Type u) :=
  { toRingHom := CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯), commutes' := ⋯ }
⊢ ∀ (x : (↑Γ(X, V) : Type u)),
    Eq (α := (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
          ((ψ₁ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
        (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.app i W) : (a : (↑Γ(Z, W) : Type u)) → (↑Γ(Z', i ⁻¹ᵁ W) : Type u))
          ((ψ₂ : (a : (↑Γ(X, V) : Type u)) → (↑Γ(Z, W) : Type u)) x : (↑Γ(Z, W) : Type u)) :
        (↑Γ(Z', i ⁻¹ᵁ W) : Type u))

Tactic:
simp [ψ₁, ψ₂, ← CategoryTheory.comp_apply, -CommRingCat.hom_comp, hig,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.appLE_comp_appLE, - Scheme.Hom.comp_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, CommRingCat.hom_comp, CategoryTheory.comp_apply, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
⊢ FormallyUnramified f

Tactic:
⟨fun {U hU V hV hVU} ↦ ?_⟩

Premises used: AlgebraicGeometry.FormallyUnramified.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
refine :
  ∀ {U : Y.Opens} {hU : IsAffineOpen U} {V : X.Opens} {hV : IsAffineOpen V} {hVU : V ≤ f ⁻¹ᵁ U},
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified
⊢ FormallyUnramified f

Tactic:
refine ⟨fun {U hU V hV hVU} ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified

Tactic:
Algebra.FormallyUnramified.iff_comp_injective.mpr fun R _ _ I hI g₁ g₂ hg₁g₂ ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyUnramified.iff_comp_injective, RingHom.FormallyUnramified
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
refine :
  ∀ (R : Type u) (x : CommRing R) (x_1 : Algebra (↑Γ(Y, U) : Type u) R) (I : Ideal R) (hI : HPow.hPow (β := ℕ) I 2 = ⊥)
    (g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R)
    (hg₁g₂ :
      Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
        (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
        (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)),
    g₁ = g₂
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified

Tactic:
refine Algebra.FormallyUnramified.iff_comp_injective.mpr fun R _ _ I hI g₁ g₂ hg₁g₂ ↦ ?_

Premises used: Iff.mpr, Algebra.FormallyUnramified.iff_comp_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
⊢ Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))

Tactic:
have hg₁ : f.appLE U V hVU ≫ CommRingCat.ofHom g₁ = CommRingCat.ofHom (algebraMap _ R) :=
    CommRingCat.hom_ext g₁.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))

Tactic:
have hg₂ : f.appLE U V hVU ≫ CommRingCat.ofHom g₂ = CommRingCat.ofHom (algebraMap _ R) :=
    CommRingCat.hom_ext g₂.comp_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ HPow.hPow (α := Ideal (↑(CommRingCat.of R) : Type u)) (β := ℕ)
      (RingHom.ker (F := (↑(CommRingCat.of R) : Type u) →+* (↑(CommRingCat.of (R ⧸ I)) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom (↑(Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) : R →+* R ⧸ I))))
      2 =
    ⊥

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ Eq (α := Spec (CommRingCat.of (R ⧸ I)) ⟶ X)
    (CategoryStruct.comp (Y := Spec (CommRingCat.of R))
      (Spec.map (CommRingCat.ofHom (↑(Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) : R →+* R ⧸ I)))
      (Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec))
    (CategoryStruct.comp (Y := Spec (CommRingCat.of R))
      (Spec.map (CommRingCat.ofHom (↑(Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) : R →+* R ⧸ I)))
      (Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec))

Tactic:
simp only [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, ← AlgHom.comp_toRingHom, *]

Premises used: AlgHom.comp_toRingHom, AlgebraicGeometry.Spec.map_comp_assoc, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ Eq (α := Spec (CommRingCat.of R) ⟶ Y)
    ((Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec) ≫ f)
    ((Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec) ≫ f)

Tactic:
simp only [Category.assoc, ← hU.SpecMap_appLE_fromSpec f hV hVU, ← Spec.map_comp_assoc, *]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
Goal:
X Y : Scheme
f : X ⟶ Y
H :
  ∀ (R S : CommRingCat.{u}) (φ : R ⟶ S),
    Function.Surjective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ) :
          (a : (↑R : Type u)) → (↑S : Type u)) →
      HPow.hPow (α := Ideal (↑R : Type u)) (β := ℕ) (RingHom.ker (CommRingCat.Hom.hom φ)) 2 = ⊥ →
        ∀ (g₁ g₂ : Spec R ⟶ X), Spec.map φ ≫ g₁ = Spec.map φ ≫ g₂ → g₁ ≫ f = g₂ ≫ f → g₁ = g₂
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
R : Type u
x : CommRing R
x_1 : Algebra (↑Γ(Y, U) : Type u) R
I : Ideal R
hI : HPow.hPow (β := ℕ) I 2 = ⊥
g₁ g₂ : (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R
hg₁g₂ :
  Eq (α := (↑Γ(X, V) : Type u) →ₐ[(↑Γ(Y, U) : Type u)] R ⧸ I)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₁)
    (AlgHom.comp (Ideal.Quotient.mkₐ (↑Γ(Y, U) : Type u) I) g₂)
hg₁ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
hg₂ :
  Eq (α := Γ(Y, U) ⟶ CommRingCat.of R)
    (Scheme.Hom.appLE f U V hVU ≫ CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R))
    (CommRingCat.ofHom (algebraMap (↑(Y.presheaf.1 (op U)) : Type u) R))
⊢ Eq (α := Spec (CommRingCat.of R) ⟶ X)
    (Spec.map (CommRingCat.ofHom (↑g₁ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)
    (Spec.map (CommRingCat.ofHom (↑g₂ : (↑(X.presheaf.1 (op V)) : Type u) →+* R)) ≫ hV.fromSpec)

Tactic:
have := H (.of R) (.of (R ⧸ I)) (CommRingCat.ofHom (Ideal.Quotient.mkₐ Γ(Y, U) I))
    Ideal.Quotient.mk_surjective (by simpa)
    (Spec.map (CommRingCat.ofHom g₁) ≫ hV.fromSpec) (Spec.map (CommRingCat.ofHom g₂) ≫ hV.fromSpec)
    (by simp only [← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp, ← AlgHom.comp_toRingHom, *])
    (by simp only [Category.assoc, ← hU.SpecMap_appLE_fromSpec f hV hVU, ← Spec.map_comp_assoc, *])