Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsConnected s ↔
    ∀ (U : Finset (Set α)),
      (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
        (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.rwSeq
     "rw"
     (Tactic.optConfig [])
     (Tactic.rwRuleSeq
      "["
      [(Tactic.rwRule [] `IsConnected) "," (Tactic.rwRule [] `isPreconnected_iff_subset_of_disjoint)]
      "]")
     [])
    []
    (Tactic.refine
     "refine"
     (Term.anonymousCtor
      "⟨"
      [(Term.fun
        "fun"
        (Term.basicFun
         [(Term.anonymousCtor "⟨" [`hne "," `h] "⟩") `U `hU `hUo `hsU]
         []
         "=>"
         (Term.syntheticHole "?" "_")))
       ","
       (Term.fun
        "fun"
        (Term.basicFun
         [`h]
         []
         "=>"
         (Term.anonymousCtor
          "⟨"
          [(Term.syntheticHole "?" "_")
           ","
           (Term.fun "fun" (Term.basicFun [`u `v `hu `hv `hs `hsuv] [] "=>" (Term.syntheticHole "?" "_")))]
          "⟩")))]
      "⟩"))
    []
    (Lean.cdot
     (Lean.cdotTk "·")
     (Tactic.tacticSeq
      (Tactic.tacticSeq1Indented
       [(Tactic.induction
         "induction"
         [(Tactic.elimTarget [] `U)]
         ["using" `Finset.induction_on]
         []
         [(Tactic.inductionAlts
           "with"
           []
           [(Tactic.inductionAlt
             [(Tactic.inductionAltLHS "|" (group [] `empty) [])]
             ["=>"
              (Tactic.tacticSeq
               (Tactic.tacticSeq1Indented
                [(Tactic.exact
                  "exact"
                  (Term.app
                   `absurd
                   [(Term.paren
                     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                     (Term.byTactic
                      "by"
                      (Tactic.tacticSeq
                       (Tactic.tacticSeq1Indented
                        [(Tactic.simpa
                          "simpa"
                          []
                          []
                          (Tactic.simpaArgsRest (Tactic.optConfig []) [] [] [] ["using" `hsU]))])))
                     ")")
                    `hne.not_subset_empty]))]))])
            (Tactic.inductionAlt
             [(Tactic.inductionAltLHS "|" (group [] `insert) [`u `U `uU `IH])]
             ["=>"
              (Tactic.tacticSeq
               (Tactic.tacticSeq1Indented
                [(Tactic.simp
                  "simp"
                  (Tactic.optConfig [])
                  []
                  ["only"]
                  ["["
                   [(Tactic.simpLemma [] ["←"] `forall_cond_comm)
                    ","
                    (Tactic.simpLemma [] [] `Finset.forall_mem_insert)
                    ","
                    (Tactic.simpLemma [] [] `Finset.exists_mem_insert)
                    ","
                    (Tactic.simpLemma [] [] `Finset.coe_insert)
                    ","
                    (Tactic.simpLemma [] [] `sUnion_insert)
                    ","
                    (Tactic.simpLemma [] [] `implies_true)
                    ","
                    (Tactic.simpLemma [] [] `true_and)]
                   "]"]
                  [(Tactic.location "at" (Tactic.locationWildcard "*"))])
                 []
                 (Tactic.refine
                  "refine"
                  (Term.app
                   (Term.proj
                    (Term.paren
                     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                     (Term.app
                      `h
                      [(Term.hole "_")
                       (Term.proj `hUo "." (fieldIdx "1"))
                       (Term.paren
                        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                        (Set.«term⋃₀_» "⋃₀" (coeNotation "↑" `U))
                        ")")
                       (Term.paren
                        (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                        (Term.app `isOpen_sUnion [(Term.proj `hUo "." (fieldIdx "2"))])
                        ")")
                       `hsU
                       (Term.syntheticHole "?" "_")])
                     ")")
                    "."
                    `imp_right)
                   [(Term.syntheticHole "?" "_")]))
                 []
                 (Lean.cdot
                  (Lean.cdotTk "·")
                  (Tactic.tacticSeq
                   (Tactic.tacticSeq1Indented
                    [(Tactic.refine
                      "refine"
                      (Term.app
                       (Term.proj `subset_empty_iff "." (fieldIdx "1"))
                       [(Term.fun
                         "fun"
                         (Term.basicFun
                          [`x (Term.anonymousCtor "⟨" [`hxs "," `hxu "," `v "," `hvU "," `hxv] "⟩")]
                          []
                          "=>"
                          (Term.syntheticHole "?" "_")))]))
                     []
                     (Tactic.exact
                      "exact"
                      (Term.app
                       `ne_of_mem_of_not_mem
                       [`hvU
                        `uU
                        (Term.proj
                         (Term.paren
                          (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                          (Term.app
                           (Term.proj `hU "." (fieldIdx "1"))
                           [`v `hvU (Term.anonymousCtor "⟨" [`x "," `hxs "," `hxu "," `hxv] "⟩")])
                          ")")
                         "."
                         `symm)]))])))
                 []
                 (Lean.cdot
                  (Lean.cdotTk "·")
                  (Tactic.tacticSeq
                   (Tactic.tacticSeq1Indented
                    [(Tactic.exact
                      "exact"
                      (Term.app
                       `IH
                       [(Term.paren
                         (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                         (Term.fun
                          "fun"
                          (Term.basicFun
                           [`u `hu]
                           []
                           "=>"
                           (Term.proj
                            (Term.paren
                             (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                             (Term.app (Term.proj `hU "." (fieldIdx "2")) [`u `hu])
                             ")")
                            "."
                            (fieldIdx "2"))))
                         ")")
                        (Term.proj `hUo "." (fieldIdx "2"))]))])))]))])])])])))
    []
    (Lean.cdot
     (Lean.cdotTk "·")
     (Tactic.tacticSeq
      (Tactic.tacticSeq1Indented
       [(Tactic.simpa
         "simpa"
         []
         []
         (Tactic.simpaArgsRest
          (Tactic.optConfig [])
          []
          []
          [(Tactic.simpArgs
            "["
            [(Tactic.simpLemma [] [] `subset_empty_iff) "," (Tactic.simpLemma [] [] `nonempty_iff_ne_empty)]
            "]")]
          ["using" (Term.app `h [(«term∅» "∅")])]))])))
    []
    (Lean.cdot
     (Lean.cdotTk "·")
     (Tactic.tacticSeq
      (Tactic.tacticSeq1Indented
       [(Tactic.rwSeq
         "rw"
         (Tactic.optConfig [])
         (Tactic.rwRuleSeq "[" [(Tactic.rwRule ["←"] `not_nonempty_iff_eq_empty)] "]")
         [(Tactic.location "at" (Tactic.locationHyp [`hsuv]))])
        []
        (Tactic.tacticHave__
         "have"
         (Term.letConfig [])
         (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" `hsuv)))
        ";"
        (Tactic.rwSeq
         "rw"
         (Tactic.optConfig [])
         (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] (Term.app `inter_comm [`u]))] "]")
         [(Tactic.location "at" (Tactic.locationHyp [`this]))])
        []
        (Tactic.simpa
         "simpa"
         []
         []
         (Tactic.simpaArgsRest
          (Tactic.optConfig [])
          []
          []
          [(Tactic.simpArgs
            "["
            [(Tactic.simpStar "*") "," (Tactic.simpLemma [] [] `or_imp) "," (Tactic.simpLemma [] [] `forall_and)]
            "]")]
          ["using"
           (Term.app
            `h
            [(choice
              («term{_}» "{" [`u "," `v] "}")
              (Term.structInst
               "{"
               []
               (Term.structInstFields
                [(Term.structInstField (Term.structInstLVal `u []) [])
                 ","
                 (Term.structInstField (Term.structInstLVal `v []) [])])
               (Term.optEllipsis [])
               []
               "}"))])]))])))])))

Goal state after: