-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
/-- A variant of `topologically_isLocalAtTarget`
that takes one iff statement instead of two implications. -/
lemma topologically_isLocalAtTarget' [(topologically P).RespectsIso]
    (hP : ∀ {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) {ι : Type u}
      (U : ι → Opens β) (_ : IsOpenCover U) (_ : Continuous f),
      P f ↔ (∀ i, P ((U i).carrier.restrictPreimage f))) :
    IsLocalAtTarget (topologically P)

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f →
      IsOpen s →
        (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f →
          (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (s.restrictPreimage f)

Tactic:
introv hf hs H

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 : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ P (s.restrictPreimage f)

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ IsOpenCover (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)

Tactic:
rw [IsOpenCover, ← top_le_iff]

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 : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ ⊤ ≤ iSup (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ ⊤ ≤ iSup (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)

Tactic:
exact le_iSup (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ⟨0⟩

Result:
no goals

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝² : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ P (s.restrictPreimage f)

Tactic:
refine (hP f (![⊤, Opens.mk s hs] ∘ Equiv.ulift) ?_ hf).mp H ⟨1⟩

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 : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
α β : Type u
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set β
hf : Continuous f
hs : IsOpen s
H : P f
⊢ IsOpenCover (![⊤, { carrier := s, is_open' := hs }] ∘ ⇑Equiv.ulift)

Proof state:
P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop
inst✝ : (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
hP :
  ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ IsLocalAtTarget (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)

Tactic:
refine topologically_isLocalAtTarget P ?_ (fun f _ U hU hU' ↦ (hP f U hU hU').mpr)

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 : α → β) {ι : Type u} (U : ι → Opens β),
    IsOpenCover U → Continuous f → (P f ↔ ∀ (i : ι), P ((U i).carrier.restrictPreimage f))
⊢ ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
    Continuous f →
      IsOpen s →
        (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) f →
          (fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P) (s.restrictPreimage f)