-- Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean
private lemma respects_isOpenImmersion_aux
    (hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource Q)
    {X Y : Scheme.{u}} [IsAffine Y] {U : Y.Opens}
    (f : X ⟶ U.toScheme) (hf : P f) : P (f ≫ U.ι)

Proof state:
case inr.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ∀ (i : ↑Us), P ((V i).ι ≫ f ≫ U.ι)

Tactic:
intro s

Result:
case inr.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
⊢ P ((V s).ι ≫ f ≫ U.ι)

Proof state:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
hYa : ∃ a, U = Y.basicOpen a
⊢ P (f ≫ U.ι)

Tactic:
obtain ⟨a, rfl⟩ := hYa

Result:
case intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
⊢ P (f ≫ (Y.basicOpen a).ι)

Proof state:
case inr.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ⨆ i, U.ι ⁻¹ᵁ ↑i = ⊤

Tactic:
apply U.ι.image_injective

Result:
case inr.intro.intro.a
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ (fun x => U.ι ''ᵁ x) (⨆ i, U.ι ⁻¹ᵁ ↑i) = (fun x => U.ι ''ᵁ x) ⊤

Proof state:
case inr.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
⊢ P ((V s).ι ≫ f ≫ U.ι)

Tactic:
let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
  (by simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι,
    Opens.map_coe, Set.image_preimage_eq_iff, heq, Opens.coe_sSup] using le_sSup s.2)

Result:
case inr.intro.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
⊢ P ((V s).ι ≫ f ≫ U.ι)

Proof state:
case inr.intro.intro.a
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ (fun x => U.ι ''ᵁ x) (⨆ i, U.ι ⁻¹ᵁ ↑i) = (fun x => U.ι ''ᵁ x) ⊤

Tactic:
simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inter, Scheme.Opens.opensRange_ι]

Result:
case inr.intro.intro.a
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
⊢ ⨆ i, U ⊓ ↑i = U.ι ''ᵁ ⊤

Proof state:
case inr.intro.intro.refine_2.intro
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => Q
X Y : Scheme
inst✝ : IsAffine Y
U : Y.Opens
f : X ⟶ ↑U
hf : P f
this : ∀ {X Y : Scheme} [inst : IsAffine Y] {U : Y.Opens} (f : X ⟶ ↑U), P f → (∃ a, U = Y.basicOpen a) → P (f ≫ U.ι)
hYa : ¬∃ a, U = Y.basicOpen a
Us : Set Y.Opens
hUs : Us ⊆ Set.range Y.basicOpen
heq✝ : U = sSup Us
V : ↑Us → X.Opens := fun s => f ⁻¹ᵁ U.ι ⁻¹ᵁ ↑s
s : ↑Us
f' : ↑(V s) ⟶ ↑(U.ι ⁻¹ᵁ ↑s) := f ∣_ U.ι ⁻¹ᵁ ↑s
hf' : P f'
e : ↑(U.ι ⁻¹ᵁ ↑s) ≅ ↑↑s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ ↑s).ι ≫ U.ι) (↑s).ι ⋯
heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ (↑s).ι
a : ↑Γ(Y, ⊤)
ha : Y.basicOpen a = ↑s
⊢ ∃ a, ↑s = Y.basicOpen a

Tactic:
use a, ha.symm

Result:
no goals