-- 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:
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)
⊢ P f

Tactic:
let g : X ⟶ (⨆ i, U i : Y.Opens) := IsOpenImmersion.lift (Scheme.Opens.ι _) f (by simpa using H)

Result:
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 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 ⋯
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯)

Tactic:
rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := P) (U := fun i : ι ↦ (⨆ i, U i).ι ⁻¹ᵁ U i)]

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 : ι), P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

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 = ⊤

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
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

Tactic:
let e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) :=
    Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE (le_iSup U i)) <| by
  simp [← CategoryTheory.cancel_mono (U i).ι, 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
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)

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 ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
⊢ (X.isoOfEq heq).hom ≫ (Arrow.mk (f ∣_ U i)).hom =
    (Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)).hom ≫ (Scheme.Opens.isoOfLE ⋯).hom

Tactic:
simp [← CategoryTheory.cancel_mono (U i).ι, g]

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 ⋯
i : ι
⊢ g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i

Tactic:
show (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = _

Result:
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 : ι
⊢ (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = f ⁻¹ᵁ U i

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 f

Tactic:
rw [← IsOpenImmersion.lift_fac (⨆ i, U i).ι f (by simpa using H)]

Result:
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).ι)

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:
intro i

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 : ι
⊢ P (IsOpenImmersion.lift (⨆ i, U i).ι f ⋯ ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i)

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 ⋯
i : ι
⊢ (g ≫ (⨆ i, U i).ι) ⁻¹ᵁ U i = f ⁻¹ᵁ U i

Tactic:
simp [g]

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 ⋯
⊢ Set.range ⇑(ConcreteCategory.hom f.base) ⊆ Set.range ⇑(ConcreteCategory.hom (⨆ i, U i).ι.base)

Tactic:
simpa using H

Result:
no goals