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