-- 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 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

case h.up.true
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 := true }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      s =
    (ConcreteCategory.hom (F.val.map (if h : { down := true }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      t

Tactic:
any_goals exact h₁

Result:
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

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
⊢ (U₁ ≤ ⨆ t, if t.down = true then U₁ else U₂) ∧ U₂ ≤ ⨆ t, if t.down = true then U₁ else U₂

Tactic:
constructor

Result:
case hcover.left
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₂

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₂

Proof state:
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 (if h : i.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
      (ConcreteCategory.hom (F.val.map (if h : i.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t

Tactic:
rintro ⟨_ | _⟩

Result:
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

case h.up.true
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 := true }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      s =
    (ConcreteCategory.hom (F.val.map (if h : { down := true }.down = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op))
      t