-- Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
theorem eq_of_locally_eq₂ {U₁ U₂ V : Opens X} (i₁ : U₁ ⟶ V) (i₂ : U₂ ⟶ V) (hcover : V ≤ U₁ ⊔ U₂)
    (s t : ToType (F.1.obj (op V))) (h₁ : F.1.map i₁.op s = F.1.map i₁.op t)
    (h₂ : F.1.map i₂.op s = F.1.map i₂.op t) : s = t

Proof state:
case hcover
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ V ≤ ⨆ t, if t.down = true then U₁ else U₂

Tactic:
refine le_trans hcover ?_

Result:
case hcover
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ U₁ ⊔ U₂ ≤ ⨆ t, if t.down = true then U₁ else U₂

Proof state:
case h.up.false
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ (ConcreteCategory.hom (F.val.map (if h : { down := false }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      s =
    (ConcreteCategory.hom (F.val.map (if h : { down := false }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      t

Tactic:
exact h₂

Result:
no goals

Proof state:
case h.up.false
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ (ConcreteCategory.hom (F.val.map (if h : { down := false }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      s =
    (ConcreteCategory.hom (F.val.map (if h : { down := false }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      t

Tactic:
any_goals exact h₂

Result:
no goals

Proof state:
case iUV
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ (i : ULift.{v, 0} Bool) → (if i.down = true then U₁ else U₂) ⟶ V

Tactic:
exact fun i => if h : i.1 then eqToHom (if_pos h) ≫ i₁ else eqToHom (if_neg h) ≫ i₂

Result:
no goals

Proof state:
case hcover.right
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ U₂ ≤ ⨆ t, if t.down = true then U₁ else U₂

Tactic:
exact le_iSup (fun t : ULift Bool => if t.1 then U₁ else U₂) (ULift.up false)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ s = t

Tactic:
fapply F.eq_of_locally_eq' fun t : ULift Bool => if t.1 then U₁ else U₂

Result:
case iUV
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ (i : ULift.{v, 0} Bool) → (if i.down = true then U₁ else U₂) ⟶ V

case hcover
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ V ≤ ⨆ t, if t.down = true then U₁ else U₂

case h
C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimits C
inst✝¹ : HasForget.forget.ReflectsIsomorphisms
inst✝ : PreservesLimits HasForget.forget
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.val.obj (op V))
h₁ : (ConcreteCategory.hom (F.val.map i₁.op)) s = (ConcreteCategory.hom (F.val.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.val.map i₂.op)) s = (ConcreteCategory.hom (F.val.map i₂.op)) t
⊢ ∀ (i : ULift.{v, 0} Bool),
    (ConcreteCategory.hom (F.val.map (Quiver.Hom.op (?iUV i)))) s =
      (ConcreteCategory.hom (F.val.map (Quiver.Hom.op (?iUV i)))) t