case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G = ⊤ → IsIso (ι G)

case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ IsIso (ι G) → G = ⊤
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G = ⊤ ↔ IsIso (ι G)
constructor
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G' : Subpresheaf F
⊢ IsIso (ι ⊤)
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ G = ⊤ → IsIso (ι G)
rintro rfl
no goals
case mp
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G' : Subpresheaf F
⊢ IsIso (ι ⊤)
infer_instance
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
⊢ G = ⊤
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
⊢ IsIso (ι G) → G = ⊤
intro H
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U ↔ x ∈ obj ⊤ U
case mpr
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
⊢ G = ⊤
ext (U x)
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U ↔ x ∈ obj ⊤ U
apply iff_true_iff.mpr
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ (forget (Type w)).map ((ι G).app U)
      ((forget (Type w)).map
        (Classical.choose (_ : ∃ inv, (ι G).app U ≫ inv = 𝟙 ((toPresheaf G).obj U) ∧ inv ≫ (ι G).app U = 𝟙 (F.obj U)))
        x) ∈
    obj G U
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ x ∈ obj G U
rw [← IsIso.inv_hom_id_apply (G.ι.app U) x]
no goals
case mpr.obj.h.h
C : Type u
inst✝ : Category C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subpresheaf F
H : IsIso (ι G)
U : Cᵒᵖ
x : F.obj U
⊢ (forget (Type w)).map ((ι G).app U)
      ((forget (Type w)).map
        (Classical.choose (_ : ∃ inv, (ι G).app U ≫ inv = 𝟙 ((toPresheaf G).obj U) ∧ inv ≫ (ι G).app U = 𝟙 (F.obj U)))
        x) ∈
    obj G U
exact ((inv (G.ι.app U)) x).2