-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
lemma injective_germ_basicOpen (U : X.Opens) (hU : IsAffineOpen U)
    (x : X) (hx : x ∈ U) (f : Γ(X, U))
    (hf : x ∈ X.basicOpen f)
    (H : Function.Injective (X.presheaf.germ U x hx)) :
    Function.Injective (X.presheaf.germ (X.basicOpen f) x hf)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
⊢ t = 0

Tactic:
have := hU.isLocalization_basicOpen f

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ t = 0

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

case intro.intro.hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

Tactic:
swap

Result:
case intro.intro.hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ U x hx))
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero] at H ⊢

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
⊢ ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
    (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) x_1 = 0 → x_1 = 0

Proof state:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
      (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s) =
    0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

Tactic:
rw [← RingHom.mem_ker, IsLocalization.mk'_eq_mul_mk'_one, Ideal.mul_unit_mem_iff_mem,
  RingHom.mem_ker, RingHom.algebraMap_toAlgebra, TopCat.Presheaf.germ_res_apply] at ht

Result:
case intro.intro
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht : (ConcreteCategory.hom (X.presheaf.germ U x ⋯)) t = 0
⊢ IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t s = 0

case intro.intro.hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
⊢ ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))),
    (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) x_1 = 0 → x_1 = 0

Tactic:
intros t ht

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
t : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))
ht : (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf)) t = 0
⊢ t = 0

Proof state:
case intro.intro.hy
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
f : ↑Γ(X, U)
hf : x ∈ X.basicOpen f
H : ∀ (x_1 : ↑(X.presheaf.obj (Opposite.op U))), (ConcreteCategory.hom (X.presheaf.germ U x hx)) x_1 = 0 → x_1 = 0
this : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
t : ↑Γ(X, U)
s : ↥(Submonoid.powers f)
ht :
  (algebraMap ↑Γ(X, U) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) t *
      IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s ∈
    RingHom.ker (ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
⊢ IsUnit (IsLocalization.mk' (↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))) 1 s)

Tactic:
exact @isUnit_of_invertible _ _ _ (@IsLocalization.invertible_mk'_one ..)

Result:
no goals