-- Mathlib/AlgebraicGeometry/SpreadingOut.lean
/--
Suppose `X` is a scheme, `x : X` such that the germ map at `x` is (locally) injective,
and `U` is a neighborhood of `x`.
Given a commutative diagram of `CommRingCat`
```
R ⟶ Γ(X, U)
↓    ↓
A ⟶ 𝒪_{X, x}
```
such that `R` is of finite type over `A`, we may lift `A ⟶ 𝒪_{X, x}` to some `A ⟶ Γ(X, V)`.
-/
lemma exists_lift_of_germInjective {x : X} [X.IsGermInjectiveAt x] {U : X.Opens} (hxU : x ∈ U)
    (φ : A ⟶ X.presheaf.stalk x) (φRA : R ⟶ A) (φRX : R ⟶ Γ(X, U))
    (hφRA : RingHom.FiniteType φRA.hom)
    (e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU) :
    ∃ (V : X.Opens) (hxV : x ∈ V) (φ' : A ⟶ Γ(X, V)) (i : V ≤ U), IsAffineOpen V ∧
      φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_2.hf.a.a.a
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ ↑(e ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a)) =
    ↑(((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) (φRA.hom' a))

Tactic:
show X.presheaf.germ _ _ _ (X.presheaf.map _ _) = (φRA ≫ φ) a

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_2.hf.a.a.a
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ (ConcreteCategory.hom (X.presheaf.germ V' x hxV')) ((ConcreteCategory.hom (X.presheaf.map ⋯.hom.op)) (φRX.hom' a)) =
    (ConcreteCategory.hom (φRA ≫ φ)) a

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_1.hf.a
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑A
⊢ (CommRingCat.Hom.hom φ) a =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (e.symm.toRingHom.comp
              ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯)) ≫
          X.presheaf.germ V' x hxV'))
      a

Tactic:
show φ a = (e (e.symm _)).1

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_1.hf.a
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑A
⊢ (ConcreteCategory.hom φ) a =
    ↑(e (e.symm (((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) a)))

Proof state:
case intro.intro.intro.intro.intro.intro.intro.refine_2
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
⊢ φRX ≫ X.presheaf.map ⋯.hom.op =
    φRA ≫
      CommRingCat.ofHom
        (e.symm.toRingHom.comp
          ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯))

Tactic:
ext a

Result:
case intro.intro.intro.intro.intro.intro.intro.refine_2.hf.a
X : Scheme
R A : CommRingCat
x : ↑↑X.toPresheafedSpace
inst✝ : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e✝ : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H : Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ V' x hxV'))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range ≤ (CommRingCat.Hom.hom f).range
e : ↑(X.presheaf.obj (Opposite.op V')) ≃+* ↥(ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range :=
  RingEquiv.ofLeftInverse ⋯
a : ↑R
⊢ (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map ⋯.hom.op)) a =
    (CommRingCat.Hom.hom
        (φRA ≫
          CommRingCat.ofHom
            (e.symm.toRingHom.comp
              ((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯))))
      a