-- Mathlib/AlgebraicGeometry/Morphisms/Basic.lean
lemma of_range_subset_iSup [P.RespectsRight @IsOpenImmersion] {ι : Type*} (U : ι → Y.Opens)
    (H : Set.range f.base ⊆ (⨆ i, U i : Y.Opens)) (hf : ∀ i, P (f ∣_ U i)) : P f

Proof state:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

Tactic:
rw [P.arrow_mk_iso_iff e]

Result:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (f ∣_ U i)

Proof state:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i = ⊤

Tactic:
apply (⨆ i, U i).ι.image_injective

Result:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ (fun x => (⨆ i, U i).ι ''ᵁ x) (⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i) = (fun x => (⨆ i, U i).ι ''ᵁ x) ⊤

Proof state:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ (⨆ i, U i).ι ''ᵁ ⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i = (⨆ i, U i).ι ''ᵁ ⊤

Tactic:
rw [Scheme.Hom.image_iSup, Scheme.Hom.image_top_eq_opensRange, Scheme.Opens.opensRange_ι]

Result:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i

Proof state:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

Tactic:
have heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i := by
  show (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _
  simp [g]

Result:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

Proof state:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ ⨆ i, (⨆ i, U i).ι ''ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = ⨆ i, U i

Tactic:
simp [Scheme.Hom.image_preimage_eq_opensRange_inter, le_iSup U]

Result:
no goals

Proof state:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (f ∣_ U i)

Tactic:
exact hf i

Result:
no goals

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ≫ (⨆ i, U i).ι)

Tactic:
apply MorphismProperty.RespectsRight.postcomp (Q := @IsOpenImmersion) _ inferInstance

Result:
case hf
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯)

Proof state:
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ Set.range ⇑(ConcreteCategory.hom (⨆ i, U i).ι.base)

Tactic:
simpa using H

Result:
no goals

Proof state:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ (fun x => (⨆ i, U i).ι ''ᵁ x) (⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i) = (fun x => (⨆ i, U i).ι ''ᵁ x) ⊤

Tactic:
dsimp

Result:
case hf.a
P : MorphismProperty Scheme
hP : IsLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight @IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑(ConcreteCategory.hom f.base) ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
⊢ (⨆ i, U i).ι ''ᵁ ⨆ i, (⨆ i, U i).ι ⁻¹ᵁ U i = (⨆ i, U i).ι ''ᵁ ⊤