awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
rw : (↑(0 * Scheme.Hom.ker i).support : Set ↥Z) = Set.univ
⊢ IsDominant i

Tactic:
rw [isDominant_iff, denseRange_iff_closure_range, ← i.support_ker,
      ← i.ker.support_pow (n + 1) (by simp), pow_succ, hn]

Premises used: pow_succ, AlgebraicGeometry.Scheme.Hom.ker, AlgebraicGeometry.isDominant_iff, HAdd.hAdd, denseRange_iff_closure_range, AlgebraicGeometry.Scheme.Hom.support_ker, AlgebraicGeometry.Scheme.IdealSheafData.support_pow, OfNat.ofNat
-- 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
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ (↑(0 * Scheme.Hom.ker i).support : Set ↥Z) = Set.univ

Tactic:
simp
-- 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
⊢ IsDominant i

Tactic:
have : IsDominant i := by
    obtain ⟨n, hn⟩ := hi
    rw [isDominant_iff, denseRange_iff_closure_range, ← i.support_ker,
      ← i.ker.support_pow (n + 1) (by simp), pow_succ, hn]
    simp
-- 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 : IsDominant i
⊢ g₁ = g₂

Tactic:
Scheme.hom_ext_of_forall _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.hom_ext_of_forall
-- 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 : IsDominant i
refine : ∀ (x : ↥Z), ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
⊢ g₁ = g₂

Tactic:
refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.hom_ext_of_forall
-- 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 : IsDominant i
x : ↥Z
obtain :
  ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)),
    ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f (g₁ x))) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : IsDominant i
x : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x : ↥X) : ↥Y)
obtain :
  ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x : ↥X))
    (hVU : V ≤ f ⁻¹ᵁ U), ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU : V ≤ f ⁻¹ᵁ U⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.isBasis_affineOpens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : 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
w : ∀ (x : ↥Z), Eq (α := ↥X) (g₁ x : ↥X) (g₂ x : ↥X)
⊢ g₁.base = g₂.base

Tactic:
ext x
-- 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 : IsDominant i
x_1 : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x_1 : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x_1 : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z
w : ∀ (x : ↥Z'), Eq (α := ↥X) (g₁ (i x : ↥Z) : ↥X) (g₂ (i x : ↥Z) : ↥X)
⊢ Eq (α := ↥X) (g₁ x : ↥X) (g₂ x : ↥X)

Tactic:
obtain ⟨x, rfl⟩ := i.surjective x

Premises used: AlgebraicGeometry.Scheme.Hom.surjective, rfl
-- 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 : IsDominant i
x_1 : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x_1 : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x_1 : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z'
⊢ Eq (α := ↥X) (g₁ (i x : ↥Z) : ↥X) (g₂ (i x : ↥Z) : ↥X)

Tactic:
congr($hig x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- 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 : IsDominant i
x_1 : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f (g₁ x_1 : ↥X) : ↥Y)
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : Membership.mem (α := ↥X) (↑V : Set ↥X) (g₁ x_1 : ↥X)
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z'
⊢ Eq (α := ↥X) (g₁ (i x : ↥Z) : ↥X) (g₂ (i x : ↥Z) : ↥X)

Tactic:
exact congr($hig x)
-- 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 : g₁.base = g₂.base
⊢ x ∈ (↑(g₂ ⁻¹ᵁ V) : Set ↥Z)

Tactic:
simpa [← this]
-- 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 : g₁.base = g₂.base
obtain :
  ∀ (W : Opens ↥Z) (hW : W ∈ Z.affineOpens) (hxW : x ∈ (↑W : Set ↥Z)) (hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V),
    ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
obtain ⟨_, ⟨W, hW, rfl⟩, hxW, hWV : W ≤ _⟩ := Z.isBasis_affineOpens.exists_subset_of_mem_open
    (And.intro hxV (by simpa [← this])) (g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V).isOpen

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.isBasis_affineOpens, CategoryTheory.Functor.obj, Min.min, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
⟨W, hxW, ?_⟩

Premises used: And.intro, Exists.intro
-- 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 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
refine : Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂
⊢ ∃ (U : Z.Opens), x ∈ U ∧ U.ι ≫ g₁ = U.ι ≫ g₂

Tactic:
refine ⟨W, hxW, ?_⟩
-- 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 : g₁.base = g₂.base
W : Opens ↥Z
hW : W ∈ Z.affineOpens
hxW : x ∈ (↑W : Set ↥Z)
hWV : W ≤ g₁ ⁻¹ᵁ V ⊓ g₂ ⁻¹ᵁ V
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FormallyUnramified

Tactic:
have := f.formallyUnramified_appLE hU hV hVU
-- 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
grw : g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ g₁ ⁻¹ᵁ f ⁻¹ᵁ U
⊢ W ≤ (g₁ ≫ f) ⁻¹ᵁ U

Tactic:
grw [hWV, inf_le_left, hVU]

Premises used: inf_le_left
-- 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
⊢ g₁ ⁻¹ᵁ f ⁻¹ᵁ U ≤ g₁ ⁻¹ᵁ f ⁻¹ᵁ U

Tactic:
rfl
-- 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
⊢ Algebra.FormallyUnramified.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)

Tactic:
algebraize [(f.appLE U V hVU).hom,
    ((g₁ ≫ f).appLE U W (by grw [hWV, inf_le_left, hVU]; rfl)).hom]

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.CategoryStruct.comp
-- 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)
r : (↑Γ(Y, U) : Type u)
⊢ (↑(↑(CommRingCat.Hom.hom (Scheme.Hom.appLE g₁ V W ⋯)) : (↑Γ(X, V) : Type u) →* (↑Γ(Z, W) : Type u)) :
          OneHom (↑Γ(X, V) : Type u) (↑Γ(Z, W) : Type u)).toFun
      ((algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u)) r) =
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(Z, W) : Type u)) r

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CategoryTheory.comp_apply, -CommRingCat.hom_comp,
      Scheme.Hom.appLE_comp_appLE]

Premises used: CommRingCat.hom_comp, CategoryTheory.comp_apply, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- 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' := ⋯ }
r : (↑Γ(Y, U) : Type u)
⊢ (↑(↑(CommRingCat.Hom.hom (Scheme.Hom.appLE g₂ V W ⋯)) : (↑Γ(X, V) : Type u) →* (↑Γ(Z, W) : Type u)) :
          OneHom (↑Γ(X, V) : Type u) (↑Γ(Z, W) : Type u)).toFun
      ((algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u)) r) =
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Z, W) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(Z, W) : Type u)) r

Tactic:
simp [RingHom.algebraMap_toAlgebra, ← CategoryTheory.comp_apply, -CommRingCat.hom_comp,
      Scheme.Hom.appLE_comp_appLE, hgf, - Scheme.Hom.comp_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, CommRingCat.hom_comp, CategoryTheory.comp_apply, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- 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_3 : (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' := ⋯ }
this : ψ₁ = ψ₂
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂

Tactic:
simpa [ψ₁, ψ₂, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom] using
      congr(hW.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom ($this).toRingHom) ≫ hV.fromSpec)

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.IsAffineOpen.fromSpec, CategoryTheory.Iso.cancel_iso_hom_left, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, CategoryTheory.Iso.hom
-- 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' := ⋯ }
suffices : ψ₁ = ψ₂
⊢ Scheme.Opens.ι W ≫ g₁ = Scheme.Opens.ι W ≫ g₂

Tactic:
suffices ψ₁ = ψ₂ by
    simpa [ψ₁, ψ₂, -Iso.cancel_iso_hom_left, IsAffineOpen.isoSpec_hom] using
      congr(hW.isoSpec.hom ≫ Spec.map (CommRingCat.ofHom ($this).toRingHom) ≫ hV.fromSpec)
-- 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' := ⋯ }
⊢ ψ₁ = ψ₂

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

Premises used: CommRingCat.Hom.hom, Algebra.FormallyUnramified.ext', AlgebraicGeometry.Scheme.Hom.app