case iUV
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ (i : ULift Bool) → (if i.down = true then U₁ else U₂) ⟶ V

case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ V ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂

case h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ ∀ (i : ULift Bool),
    (CategoryTheory.forget C).map (F.val.map (?iUV i).op) s = (CategoryTheory.forget C).map (F.val.map (?iUV i).op) t
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ s = t
fapply F.eq_of_locally_eq' fun t : ULift Bool => if t.1 then U₁ else U₂
no goals
case iUV
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ (i : ULift Bool) → (if i.down = true then U₁ else U₂) ⟶ V
exact fun i => if h : i.1 then eqToHom (if_pos h) ≫ i₁ else eqToHom (if_neg h) ≫ i₂
case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₁ ⊔ U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ V ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
refine' le_trans hcover _
case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ (U₁ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂) ∧
    U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₁ ⊔ U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
rw [sup_le_iff]
case hcover.left
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₁ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂

case hcover.right
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
case hcover
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ (U₁ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂) ∧
    U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
constructor
no goals
case hcover.left
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₁ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
convert le_iSup (fun t : ULift Bool => if t.1 then U₁ else U₂) (ULift.up True)
no goals
case hcover.right
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ U₂ ≤ ⨆ (t : ULift Bool), if t.down = true then U₁ else U₂
convert le_iSup (fun t : ULift Bool => if t.1 then U₁ else U₂) (ULift.up False)
no goals
case h
C : Type u
inst✝⁴ : Category C
inst✝³ : ConcreteCategory C
inst✝² : HasLimits C
inst✝¹ : ReflectsIsomorphisms ConcreteCategory.forget
inst✝ : PreservesLimits ConcreteCategory.forget
X : TopCat
F : Sheaf C X
ι : Type v
U : ι → Opens ↑X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : (CategoryTheory.forget C).obj (F.val.obj V.op)
h₁ : (CategoryTheory.forget C).map (F.val.map i₁.op) s = (CategoryTheory.forget C).map (F.val.map i₁.op) t
h₂ : (CategoryTheory.forget C).map (F.val.map i₂.op) s = (CategoryTheory.forget C).map (F.val.map i₂.op) t
⊢ ∀ (i : ULift Bool),
    (CategoryTheory.forget C).map
        (F.val.map
          (if h : i.down = true then eqToHom (_ : (if i.down = true then U₁ else U₂) = U₁) ≫ i₁
            else eqToHom (_ : (if i.down = true then U₁ else U₂) = U₂) ≫ i₂).op)
        s =
      (CategoryTheory.forget C).map
        (F.val.map
          (if h : i.down = true then eqToHom (_ : (if i.down = true then U₁ else U₂) = U₁) ≫ i₁
            else eqToHom (_ : (if i.down = true then U₁ else U₂) = U₂) ≫ i₂).op)
        t
rintro ⟨_ | _⟩ <;> simp [h₁, h₂]