-- Mathlib/AlgebraicGeometry/Properties.lean
theorem isIntegral_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f]
    [IsIntegral Y] [Nonempty X] : IsIntegral X

Proof state:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ IsDomain ↑Γ(X, U)

Tactic:
have : U = f ⁻¹ᵁ f ''ᵁ U := by ext1; exact (Set.preimage_image_eq _ H.base_open.injective).symm

Result:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ IsDomain ↑Γ(X, U)

Proof state:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
have : IsDomain Γ(Y, f ''ᵁ U) := by
  apply (config := { allowSynthFailures := true }) IsIntegral.component_integral
  exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩

Result:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : U = f ⁻¹ᵁ f ''ᵁ U
this : IsDomain ↑Γ(Y, f ''ᵁ U)
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ U = f ⁻¹ᵁ f ''ᵁ U

Tactic:
ext1

Result:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ↑U = ↑(f ⁻¹ᵁ f ''ᵁ U)

Proof state:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this✝ : U = f ⁻¹ᵁ f ''ᵁ U
this : IsDomain ↑Γ(Y, f ''ᵁ U)
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
exact (asIso <| f.app (f ''ᵁ U) :
  Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.toMulEquiv.isDomain _

Result:
no goals

Proof state:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ IsDomain ↑Γ(X, U)

Tactic:
rw [this]

Result:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Proof state:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
⊢ autoParam (∀ (U : X.Opens) [inst : Nonempty ↑↑(↑U).toPresheafedSpace], IsDomain ↑Γ(X, U)) _auto✝

Tactic:
intro U hU

Result:
case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ IsDomain ↑Γ(X, U)

Proof state:
case inst
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ Nonempty ↑↑(↑(f ''ᵁ U)).toPresheafedSpace

Tactic:
exact ⟨⟨_, _, hU.some.prop, rfl⟩⟩

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ IsDomain ↑Γ(Y, f ''ᵁ U)

Tactic:
apply (config := { allowSynthFailures := true }) IsIntegral.component_integral

Result:
case inst
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ Nonempty ↑↑(↑(f ''ᵁ U)).toPresheafedSpace

Proof state:
case nonempty
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
⊢ autoParam (Nonempty ↑↑X.toPresheafedSpace) _auto✝

Tactic:
infer_instance

Result:
no goals

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
U : X.Opens
hU : Nonempty ↑↑(↑U).toPresheafedSpace
⊢ ↑U = ↑(f ⁻¹ᵁ f ''ᵁ U)

Tactic:
exact (Set.preimage_image_eq _ H.base_open.injective).symm

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
⊢ IsIntegral X

Tactic:
constructor

Result:
case nonempty
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
⊢ autoParam (Nonempty ↑↑X.toPresheafedSpace) _auto✝

case component_integral
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↑↑X.toPresheafedSpace
⊢ autoParam (∀ (U : X.Opens) [inst : Nonempty ↑↑(↑U).toPresheafedSpace], IsDomain ↑Γ(X, U)) _auto✝