Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsIrreducible s ↔
    ∀ (U : Finset (Set X)), (∀ u ∈ U, IsOpen[inst✝] u) → (∀ u ∈ U, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑U).Nonempty

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.refine
    "refine"
    (Term.anonymousCtor
     "⟨"
     [(Term.fun "fun" (Term.basicFun [`h `U `hu `hU] [] "=>" (Term.syntheticHole "?" "_")))
      ","
      (Term.fun
       "fun"
       (Term.basicFun
        [`h]
        []
        "=>"
        (Term.anonymousCtor "⟨" [(Term.syntheticHole "?" "_") "," (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.simpa
                 "simpa"
                 []
                 []
                 (Tactic.simpaArgsRest (Tactic.optConfig []) [] [] [] ["using" `h.nonempty]))]))])
           (Tactic.inductionAlt
            [(Tactic.inductionAltLHS "|" (group [] `insert) [`u `U (Term.hole "_") `IH])]
            ["=>"
             (Tactic.tacticSeq
              (Tactic.tacticSeq1Indented
               [(Tactic.rwSeq
                 "rw"
                 (Tactic.optConfig [])
                 (Tactic.rwRuleSeq
                  "["
                  [(Tactic.rwRule [] `Finset.coe_insert) "," (Tactic.rwRule [] `sInter_insert)]
                  "]")
                 [])
                []
                (Tactic.rwSeq
                 "rw"
                 (Tactic.optConfig [])
                 (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] `Finset.forall_mem_insert)] "]")
                 [(Tactic.location "at" (Tactic.locationHyp [`hu `hU]))])
                []
                (Tactic.exact
                 "exact"
                 (Term.app
                  (Term.proj `h "." (fieldIdx "2"))
                  [(Term.hole "_")
                   (Term.hole "_")
                   (Term.proj `hu "." (fieldIdx "1"))
                   (Term.paren
                    (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                    (Term.app `U.finite_toSet.isOpen_sInter [(Term.proj `hu "." (fieldIdx "2"))])
                    ")")
                   (Term.proj `hU "." (fieldIdx "1"))
                   (Term.paren
                    (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                    (Term.app `IH [(Term.proj `hu "." (fieldIdx "2")) (Term.proj `hU "." (fieldIdx "2"))])
                    ")")]))]))])])])])))
   []
   (Lean.cdot
    (Lean.cdotTk "·")
    (Tactic.tacticSeq
     (Tactic.tacticSeq1Indented
      [(Tactic.simpa
        "simpa"
        []
        []
        (Tactic.simpaArgsRest (Tactic.optConfig []) [] [] [] ["using" (Term.app `h [(«term∅» "∅")])]))])))
   []
   (Lean.cdot
    (Lean.cdotTk "·")
    (Tactic.tacticSeq
     (Tactic.tacticSeq1Indented
      [(Tactic.intro "intro" [`u `v `hu `hv `hu' `hv'])
       []
       (Tactic.simpa
        "simpa"
        []
        []
        (Tactic.simpaArgsRest
         (Tactic.optConfig [])
         []
         []
         [(Tactic.simpArgs "[" [(Tactic.simpStar "*")] "]")]
         ["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: