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