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