Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
⊢ (F.toDescentData f).IsEquivalence

Tactic:
(Tactic.tacticSeq1Indented
 [(Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId `H)
     [(Term.explicitBinder "(" [`i'] [":" `ι'] [] ")")]
     [(Term.typeSpec
       ":"
       («term∃_,_»
        "∃"
        (Lean.explicitBinders
         [(Lean.bracketedExplicitBinders "(" [(Lean.binderIdent `i)] ":" `ι ")")
          (Lean.bracketedExplicitBinders
           "("
           [(Lean.binderIdent `p)]
           ":"
           («term_⟶_» (Term.app `X' [`i']) "⟶" (Term.app `X [`i]))
           ")")])
        ","
        («term_=_» (CategoryTheory.«term_≫_» `p "≫" (Term.app `f [`i])) "=" (Term.app `f' [`i']))))]
     ":="
     (Term.byTactic
      "by"
      (Tactic.tacticSeq
       (Tactic.tacticSeq1Indented
        [(Tactic.obtain
          "obtain"
          [(Tactic.rcasesPatMed
            [(Tactic.rcasesPat.tuple
              "⟨"
              [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.ignore "_")]) [])
               ","
               (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `p)]) [])
               ","
               (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.ignore "_")]) [])
               ","
               (Tactic.rcasesPatLo
                (Tactic.rcasesPatMed
                 [(Tactic.rcasesPat.tuple
                   "⟨"
                   [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `i)]) [])]
                   "⟩")])
                [])
               ","
               (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `fac)]) [])]
              "⟩")])]
          []
          [":="
           [(Term.app
             `h₂
             [(Term.hole "_")
              (Term.paren
               (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
               (Term.app `Sieve.ofArrows_mk [(Term.hole "_") `f' `i'])
               ")")])]])
         []
         (Tactic.exact "exact" (Term.anonymousCtor "⟨" [(Term.hole "_") "," (Term.hole "_") "," `fac] "⟩"))]))))))
  []
  (Mathlib.Tactic.Choose.choose
   "choose"
   []
   [(Mathlib.Tactic.Choose.chooseBinder (Lean.binderIdent `α))
    (Mathlib.Tactic.Choose.chooseBinder (Lean.binderIdent `p))
    (Mathlib.Tactic.Choose.chooseBinder (Lean.binderIdent `hp))]
   ["using" `H])
  []
  (Tactic.obtain
   "obtain"
   [(Tactic.rcasesPatMed
     [(Tactic.rcasesPat.tuple
       "⟨"
       [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `H)]) [])
        ","
        (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `h)]) [])
        ","
        (Tactic.rcasesPatLo
         (Tactic.rcasesPatMed
          [(Tactic.rcasesPat.tuple
            "⟨"
            [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `e)]) [])]
            "⟩")])
         [])]
       "⟩")])]
   [":"
    («term∃_,_»
     "∃"
     (Lean.explicitBinders
      [(Lean.bracketedExplicitBinders
        "("
        [(Lean.binderIdent `H)]
        ":"
        (CategoryTheory.«term_⥤_» (Term.hole "_") "⥤" (Term.hole "_"))
        ")")
       (Lean.bracketedExplicitBinders "(" [(Lean.binderIdent (Term.hole "_"))] ":" `H.FullyFaithful ")")])
     ","
     (Term.app
      `Nonempty
      [(Term.paren
        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
        (CategoryTheory.«term_≅_»
         (CategoryTheory.«term_⋙_» (Term.app `F.toDescentData [`f]) "⋙" `H)
         "≅"
         (Term.app `F.toDescentData [`f']))
        ")")]))]
   [":="
    [(Term.byTactic
      "by"
      (Tactic.tacticSeq
       (Tactic.tacticSeq1Indented
        [(Tactic.refine
          "refine"
          (Term.anonymousCtor
           "⟨"
           [(Term.app
             `pullFunctor
             [`F
              (Term.namedArgument "(" `p ":=" (Term.app (CategoryTheory.«term𝟙» "𝟙") [(Term.hole "_")]) ")")
              (Term.namedArgument "(" `p' ":=" `p ")")
              (Term.paren
               (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
               (Term.byTactic
                "by"
                (Tactic.tacticSeq (Tactic.tacticSeq1Indented [(CategoryTheory.cat_disch "cat_disch")])))
               ")")])
            ","
            (Term.syntheticHole "?" "_")
            ","
            (Term.syntheticHole "?" "_")]
           "⟩"))
         []
         (Lean.cdot
          (Lean.cdotTk "·")
          (Tactic.tacticSeq
           (Tactic.tacticSeq1Indented [(Tactic.exact "exact" (Term.app `fullyFaithfulPullFunctor [`F `hp `h₁]))])))
         []
         (Lean.cdot
          (Lean.cdotTk "·")
          (Tactic.tacticSeq
           (Tactic.tacticSeq1Indented
            [(Tactic.exact
              "exact"
              (Term.anonymousCtor
               "⟨"
               [(CategoryTheory.Iso.«term_≪≫_»
                 (Term.app `toDescentDataCompPullFunctorIso [(Term.hole "_") (Term.hole "_")])
                 "≪≫"
                 (CategoryTheory.Iso.«term_≪≫_»
                  (Term.paren
                   (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                   (Term.app
                    `Functor.isoWhiskerRight
                    [(Term.paren
                      (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                      (Term.app
                       `Cat.Hom.toNatIso
                       [(Term.paren
                         (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                         (Term.app `F.mapId [(Term.hole "_")])
                         ")")])
                      ")")
                     (Term.hole "_")])
                   ")")
                  "≪≫"
                  (Term.app `Functor.leftUnitor [(Term.hole "_")])))]
               "⟩"))])))])))]])
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     []
     ":="
     (Term.proj
      (Term.paren
       (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
       (Term.app
        `F.fullyFaithfulToDescentData
        [(Term.hole "_")
         (Term.paren
          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
          (Term.app `J.superset_covering [`h₂ `h₁])
          ")")])
       ")")
      "."
      `faithful))))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     []
     ":="
     (Term.proj
      (Term.paren
       (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
       (Term.app
        `F.fullyFaithfulToDescentData
        [(Term.hole "_")
         (Term.paren
          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
          (Term.app `J.superset_covering [`h₂ `h₁])
          ")")])
       ")")
      "."
      `full))))
  []
  (Tactic.tacticHave__
   "have"
   (Term.letConfig [])
   (Term.letDecl
    (Term.letIdDecl
     (Term.letId (hygieneInfo `[anonymous]))
     []
     [(Term.typeSpec
       ":"
       (Term.proj
        (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `F.toDescentData [`f]) ")")
        "."
        `EssSurj))]
     ":="
     (Term.anonymousCtor
      "⟨"
      [(Term.fun
        "fun"
        (Term.basicFun
         [`D]
         []
         "↦"
         (Term.anonymousCtor
          "⟨"
          [(Term.hole "_")
           ","
           (Term.anonymousCtor
            "⟨"
            [(Term.app
              `h.preimageIso
              [(Term.paren
                (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                (CategoryTheory.Iso.«term_≪≫_»
                 (Term.app `e.app [(Term.hole "_")])
                 "≪≫"
                 (Term.app
                  (Term.proj
                   (Term.paren
                    (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                    (Term.app `F.toDescentData [`f'])
                    ")")
                   "."
                   `objObjPreimageIso)
                  [(Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `H.obj [`D]) ")")]))
                ")")])]
            "⟩")]
          "⟩")))]
      "⟩"))))
  []
  (Tactic.exact
   "exact"
   (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])

Goal state after: