-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- To check that a topologically defined morphism property is local at the target,
we may check the corresponding properties on topological spaces. -/
lemma topologically_isLocalAtTarget [(topologically P).RespectsIso]
    (hP₂ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set β)
      (_ : Continuous f) (_ : IsOpen s), P f → P (s.restrictPreimage f))
    (hP₃ : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u}
      (U : ι → Opens β) (_ : IsOpenCover U) (_ : Continuous f),
      (∀ i, P ((U i).carrier.restrictPreimage f)) → P f) :
    IsLocalAtTarget (topologically P)

Proof state:
case of_sSup_eq_top
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U i)
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f

Tactic:
apply hP₃ f.base U hU f.base.hom.continuous fun i ↦ ?_

Result:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U i)
i : ι
⊢ P ((U i).carrier.restrictPreimage ⇑(ConcreteCategory.hom f.base))

Proof state:
case restrict
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U)

Tactic:
simp_rw [topologically, morphismRestrict_base]

Result:
case restrict
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
⊢ P (U.carrier.restrictPreimage ⇑(ConcreteCategory.hom f.base))

Proof state:
case of_sSup_eq_top
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens),
    iSup U = ⊤ →
      (∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U i)) →
        topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f

Tactic:
intro X Y f ι U hU hf

Result:
case of_sSup_eq_top
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U i)
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f

Proof state:
case restrict
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f →
      topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U)

Tactic:
intro X Y f U hf

Result:
case restrict
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP₂ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f → IsOpen s → P f → P (s.restrictPreimage f)
hP₃ :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hf : topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (f ∣_ U)