-- Mathlib/Topology/Sheaves/Stalks.lean
theorem section_ext (F : Sheaf C X) (U : Opens X) (s t : ToType (F.1.obj (op U)))
    (h : ∀ (x : X) (hx : x ∈ U), F.presheaf.germ U x hx s = F.presheaf.germ U x hx t) : s = t

Proof state:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ U ≤ iSup V

Tactic:
intro x hxU

Result:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)

Proof state:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
⊢ ∀ (i : ↥U), (ConcreteCategory.hom (F.val.map (i₁ i).op)) s = (ConcreteCategory.hom (F.val.map (i₁ i).op)) t

Tactic:
intro x

Result:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.val.map (i₁ x).op)) s = (ConcreteCategory.hom (F.val.map (i₁ x).op)) t

Proof state:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i

Tactic:
exact ⟨⟨x, hxU⟩, m ⟨x, hxU⟩⟩

Result:
no goals

Proof state:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ ↑U
⊢ x ∈ ↑(iSup V)

Tactic:
simp only [Opens.coe_iSup, Set.mem_iUnion, SetLike.mem_coe]

Result:
case hcover
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↑X
hxU : x ∈ ↑U
⊢ ∃ i, x ∈ V i

Proof state:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F : Sheaf C X
U : Opens ↑X
s t : ToType (F.val.obj (op U))
h :
  ∀ (x : ↑X) (hx : x ∈ U),
    (ConcreteCategory.hom (F.presheaf.germ U x hx)) s = (ConcreteCategory.hom (F.presheaf.germ U x hx)) t
V : ↥U → Opens ↑X
m : ∀ (x : ↥U), ↑x ∈ V x
i₁ i₂ : (x : ↥U) → V x ⟶ U
heq :
  ∀ (x : ↥U), (ConcreteCategory.hom (F.presheaf.map (i₁ x).op)) s = (ConcreteCategory.hom (F.presheaf.map (i₂ x).op)) t
x : ↥U
⊢ (ConcreteCategory.hom (F.val.map (i₁ x).op)) s = (ConcreteCategory.hom (F.val.map (i₁ x).op)) t

Tactic:
rw [heq, Subsingleton.elim (i₁ x) (i₂ x)]

Result:
no goals