-- Mathlib/AlgebraicGeometry/Noetherian.lean
lemma isLocallyNoetherian_of_isOpenImmersion {Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f]
    [IsLocallyNoetherian Y] : IsLocallyNoetherian X

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Scheme.Hom.opensRange f ⊓ ↑V = ↑V
⊢ Γ(Y, Scheme.Hom.opensRange f ⊓ f ''ᵁ ↑U) ≅ Γ(Y, ↑V)

Tactic:
rw [this]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(X, f ⁻¹ᵁ f ''ᵁ ↑U) ≅ ?m.31540

Tactic:
apply IsOpenImmersion.ΓIso

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(Y, Scheme.Hom.opensRange f ⊓ f ''ᵁ ↑U) ≅ Γ(Y, ↑V)

Tactic:
suffices Scheme.Hom.opensRange f ⊓ V = V by
  rw [this]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Scheme.Hom.opensRange f ⊓ ↑V = ↑V

Proof state:
case convert_4
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ IsNoetherianRing ↑Γ(Y, ↑V)

Tactic:
exact IsLocallyNoetherian.component_noetherian V

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(X, f ⁻¹ᵁ f ''ᵁ ↑U) ≅ Γ(Y, ↑V)

Tactic:
trans

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(X, f ⁻¹ᵁ f ''ᵁ ↑U) ≅ ?m.31540

X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ ?m.31540 ≅ Γ(Y, ↑V)

X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ CommRingCat

Proof state:
case convert_3.e
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ Γ(Y, ↑V) ≅ Γ(X, ↑U)

Tactic:
exact this.symm

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
let V : Y.affineOpens := ⟨f ''ᵁ U, IsAffineOpen.image_of_isOpenImmersion U.prop _⟩

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(X, ↑U) ≅ Γ(Y, ↑V)

Tactic:
rw [← Scheme.Hom.preimage_image_eq f U]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Γ(X, f ⁻¹ᵁ f ''ᵁ ↑U) ≅ Γ(Y, ↑V)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Tactic:
convert isNoetherianRing_of_ringEquiv (R := Γ(Y, V)) _

Result:
case convert_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ ↑Γ(Y, ↑V) ≃+* ↑Γ(X, ↑U)

case convert_4
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ IsNoetherianRing ↑Γ(Y, ↑V)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ ↑↑U ⊆ Set.univ

Tactic:
exact Set.subset_univ _

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ ↑(Scheme.Hom.opensRange f ⊓ ↑V) = ↑↑V

Tactic:
rw [Opens.coe_inf, Scheme.Hom.coe_opensRange, IsOpenMap.coe_functor_obj,
  Set.inter_eq_right, Set.image_subset_iff, Set.preimage_range]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ ↑↑U ⊆ Set.univ

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ Scheme.Hom.opensRange f ⊓ ↑V = ↑V

Tactic:
rw [← Opens.coe_inj]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
⊢ ↑(Scheme.Hom.opensRange f ⊓ ↑V) = ↑↑V

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
⊢ IsLocallyNoetherian X

Tactic:
refine ⟨fun U => ?_⟩

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
⊢ IsNoetherianRing ↑Γ(X, ↑U)

Proof state:
case convert_3
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ ↑Γ(Y, ↑V) ≃+* ↑Γ(X, ↑U)

Tactic:
apply CategoryTheory.Iso.commRingCatIsoToRingEquiv

Result:
case convert_3.e
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsLocallyNoetherian Y
U : ↑X.affineOpens
V : ↑Y.affineOpens := ⟨f ''ᵁ ↑U, ⋯⟩
this : Γ(X, ↑U) ≅ Γ(Y, ↑V)
⊢ Γ(Y, ↑V) ≅ Γ(X, ↑U)