-- Module: Mathlib.Topology.Sheaves.Flasque
Goal:
X : TopCat
U : Opens (↑X : Type u)
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst : S.X₁.IsFlasque
s : (↑(S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) : Type u)
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty.{u + 1} (a ⟶ t) → Nonempty.{u + 1} (t ⟶ a)
tle :
  unop
      ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c)) ≤
    U
tcomp :
  Eq (α :=
    ToType (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)
      (S.X₃.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
        (op
          (unop
            ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
              (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                    CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
                c))))))
    (restrictOpen (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
      AddCommGrpCat.carrier) s
      (unop
        ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
          (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                  (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
            c)))
      tle)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
          AddCommGrpCat.carrier) (X :=
          S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
            ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
              (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                    CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
                c)))
          (S.g.hom.app
            ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
              (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
                    CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                      (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
                c))) :
        (a : (↑(S.X₂.obj.obj (StructuredArrow.right t).fst) : Type u)) →
          (↑(S.X₃.obj.obj (StructuredArrow.right t).fst) : Type u))
      ((StructuredArrow.right t).snd (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c)))
⊢ U ≤
    unop
      ((StructuredArrow.right t).fst (β := fun (c : (Opens (↑X : Type u))ᵒᵖ) ↦
        (S.X₂.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))) ⋙
              CategoryTheory.forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{u}) ↦
                (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := AddCommGrpCat.carrier)).obj
          c))

Tactic:
have : U ≤ t.right.1.unop := by
  -- Prove that the set of definition of `t.right.2` contains `U`.
    intro x hx
    have := (isLocallySurjective_iff_epi S.g).mpr hS.epi_g
    -- We use local surjectivity to find a section `t₁` of `S.X₂` on a neighborhood `W` of `x`
    -- that maps to `s |_ W` by `S.g`.
    obtain ⟨W, Wle, ⟨t₁, ht₁⟩, hW⟩ := (isLocallySurjective_iff S.g.hom).mp this U s x hx
    --`t.right.2` and `t₁` need not agree on their overlap so we need to deal with their
    -- difference `t₂`
    let t₂ := t.right.2 |_ (t.right.1.unop ⊓ W) - t₁ |_ (t.right.1.unop ⊓ W)
    have : (S.g.hom.app (op (t.right.1.unop ⊓ W))) t₂ = 0 := by
      simp [map_restrict, ← tcomp, restrict_restrict, ht₁, t₂]
    -- Since `S` is exact and `t₂` maps to zero, we can lift it to a section `t₃` of `S.X₁`
    obtain ⟨t₃, ht₃⟩ := Sheaf.sections_exact_of_left_exact hS.1 hS.2 t₂ this
    -- Using that `S.X₁` is flasque, we can lift `t₃` to a section on `W`.
    obtain ⟨t₄, (ht₄ : t₄ |_ (t.right.1.unop ⊓ W) = t₃)⟩ := (AddCommGrpCat.epi_iff_surjective
      (S.X₁.obj.map (homOfLE inf_le_right).op)).mp inferInstance t₃
    let f : Fin 2 → Opens X := ![t.right.1.unop, W]
    let sf : (i : Fin 2) → S.X₂.obj.obj (op (f i))
    | 0 => t.right.2
    | 1 => t₁ + (S.f.hom.app (op W)) t₄
    have : sf 0 |_ (t.right.1.unop ⊓ W) = sf 1 |_ (t.right.1.unop ⊓ W) := by
      dsimp [sf, f]
      simp only [restrict_sum, ← map_restrict, ht₄, ht₃, t₂, add_sub_cancel]
    -- We glue `t.right.2` and `t₁ + (S.f.hom.app (op W)) t₄` together to form `t₅`
    obtain ⟨t₅, ht₅, _⟩ : ∃! t₅, IsGluing S.X₂.obj f sf t₅ := by
      apply Sheaf.existsUnique_gluing
      simp only [IsCompatible, Fin.forall_fin_two]
      refine ⟨⟨rfl, this⟩, Eq.symm ?_, rfl⟩
      apply_fun (fun s ↦ restrictOpen s (W ⊓ t.right.1.unop) (le_of_eq (inf_comm _ _))) at this
      rw [restrict_restrict, restrict_restrict] at this
      exact this
    have le : iSup f ≤ U := iSup_le_iff.mpr (Fin.forall_fin_two.mpr ⟨tle, Wle⟩)
    -- We upgrade `t₅` to an object in `Under S.g s` that is defined on `t.right.1.unop ⊔ W`.
    let t₆ : Under S.g s :=
      StructuredArrow.mk (S := ⟨op U, s⟩)
        (T := (Functor.whiskerRight S.g.hom (CategoryTheory.forget AddCommGrpCat)).mapElements)
        (Y := ⟨op (iSup f), t₅⟩) <| CategoryOfElements.homMk _ _ (homOfLE le).op (by
          refine (eq_app_of_locally_eq ht₅ (by rw [Fin.forall_fin_two]; exact ⟨tle, Wle⟩) ?_).symm
          rw [Fin.forall_fin_two]
          refine ⟨tcomp.symm, ?_⟩
          simp only [Fin.isValue, Functor.comp_obj, map_add, homOfLE_leOfHom, sf, f]
          have : (S.f.hom.app (op W) ≫ S.g.hom.app (op W)) = 0 := by
            rw [← NatTrans.comp_app, ← ObjectProperty.FullSubcategory.comp_hom, S.zero]
            rfl
          simp [← CategoryTheory.comp_apply, this, ht₁]
          rfl)
    -- We prove that `t₆` is bigger than `t` for the preorder used on `Under S.g s`.
    have : Nonempty (t₆ ⟶ t) := Nonempty.intro (StructuredArrow.homMk (CategoryOfElements.homMk _ _
      (homOfLE (le_iSup f 0)).op (ht₅ 0)) (by cat_disch))
    exact leOfHom ((ht t₆) this).some.right.1.unop ((le_iSup f 1) hW)