-- 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
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'
⊢ ∃ V,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'

Tactic:
have hf' : RingHom.range (X.presheaf.germ V x hxV).hom ≤ RingHom.range f.hom := by
  rw [← X.presheaf.germ_res iV'V.hom _ hxV']
  exact Set.range_comp_subset_range (X.presheaf.map iV'V.hom.op) f

Result:
case intro.intro.intro.intro.intro.intro.intro
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
⊢ ∃ V,
    ∃ (hxV : 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_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)))

Tactic:
simp only [RingEquiv.apply_symm_apply]

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 =
    ↑(((CommRingCat.Hom.hom φ).codRestrict (ConcreteCategory.hom (X.presheaf.germ V' x hxV')).range ⋯) a)

Proof state:
case intro.intro.intro.intro.intro.intro.intro
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
⊢ ∃ V,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'

Tactic:
let e := RingEquiv.ofLeftInverse H.hasLeftInverse.choose_spec

Result:
case intro.intro.intro.intro.intro.intro.intro
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 ⋯
⊢ ∃ V,
    ∃ (hxV : x ∈ V),
      ∃ φ', ∃ (i : V ≤ U), IsAffineOpen V ∧ φ = φ' ≫ X.presheaf.germ V x hxV ∧ φRX ≫ X.presheaf.map i.hom.op = φRA ≫ φ'