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:
(Term.byTactic
 "by"
 (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: