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:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (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: