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