-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem to_iso [h' : Epi f.base] : IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso f

Tactic:
have : ∀ (U : (Opens Y)ᵒᵖ), IsIso (f.c.app U) := by
  intro U
  have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
    induction U using Opposite.rec' with | h U => ?_
    cases U
    dsimp only [Functor.op, Opens.map]
    congr
    exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm
  convert H.c_iso (Opens.map f.base |>.obj <| unop U)

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
⊢ IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)

Tactic:
intro U

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ IsIso (f.c.app U)

Proof state:
case h.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op
      ((opensFunctor f).obj
        { carrier := ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑{ carrier := carrier✝, is_open' := is_open'✝ },
          is_open' := ⋯ })

Tactic:
congr

Result:
case h.mk.e_unop.e_carrier
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ carrier✝ =
    ⇑(ConcreteCategory.hom f.base) ''
      ↑{ carrier := ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑{ carrier := carrier✝, is_open' := is_open'✝ }, is_open' := ⋯ }

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))

Tactic:
cases U

Result:
case h.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op { carrier := carrier✝, is_open' := is_open'✝ }))))

Proof state:
case inst
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f.base

Tactic:
let t : X ≃ₜ Y := (Homeomorph.ofIsEmbedding _ H.base_open.isEmbedding).trans
  { toFun := Subtype.val
    invFun := fun x =>
      ⟨x, by rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp h')]; trivial⟩
    left_inv := fun ⟨_, _⟩ => rfl
    right_inv := fun _ => rfl }

Result:
case inst
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
t : ↑↑X ≃ₜ ↑↑Y :=
  (Homeomorph.ofIsEmbedding ⇑(ConcreteCategory.hom f.base) ⋯).trans
    { toFun := Subtype.val, invFun := fun x => ⟨x, ⋯⟩, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
⊢ IsIso f.base

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
⊢ IsIso f

Tactic:
have : IsIso f.c := NatIso.isIso_of_isIso_app _

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
this : U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))
⊢ IsIso (f.c.app U)

Tactic:
convert H.c_iso (Opens.map f.base |>.obj <| unop U)

Result:
no goals

Proof state:
case h.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op { carrier := carrier✝, is_open' := is_open'✝ }))))

Tactic:
dsimp only [Functor.op, Opens.map]

Result:
case h.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ op { carrier := carrier✝, is_open' := is_open'✝ } =
    op
      ((opensFunctor f).obj
        { carrier := ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑{ carrier := carrier✝, is_open' := is_open'✝ },
          is_open' := ⋯ })

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ IsIso (f.c.app U)

Tactic:
have : U = op (opensFunctor f |>.obj ((Opens.map f.base).obj (unop U))) := by
  induction U using Opposite.rec' with | h U => ?_
  cases U
  dsimp only [Functor.op, Opens.map]
  congr
  exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
this : U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))
⊢ IsIso (f.c.app U)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))

Tactic:
induction U using Opposite.rec' with | h U => ?_

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : Opens ↑↑Y
⊢ op U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop (op U))))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.univ

Tactic:
trivial

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f

Tactic:
apply (config := { allowSynthFailures := true }) isIso_of_components

Result:
case inst
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
⊢ IsIso f.base

Proof state:
case h.mk.e_unop.e_carrier
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
carrier✝ : Set ↑↑Y
is_open'✝ : IsOpen carrier✝
⊢ carrier✝ =
    ⇑(ConcreteCategory.hom f.base) ''
      ↑{ carrier := ⇑(ConcreteCategory.hom f.base) ⁻¹' ↑{ carrier := carrier✝, is_open' := is_open'✝ }, is_open' := ⋯ }

Tactic:
exact (Set.image_preimage_eq _ ((TopCat.epi_iff_surjective _).mp h')).symm

Result:
no goals