Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
⊢ M.eRk X ≤ 1 ↔ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
(Tactic.tacticSeq
 (Tactic.tacticSeq1Indented
  [(Tactic.refine
    "refine"
    (Term.anonymousCtor
     "⟨"
     [(Term.fun "fun" (Term.basicFun [`h] [] "↦" (Term.syntheticHole "?" "_")))
      ","
      (Term.fun
       "fun"
       (Term.basicFun
        [(Term.anonymousCtor "⟨" [`e "," (Term.hole "_") "," `he] "⟩")]
        []
        "↦"
        (Term.syntheticHole "?" "_")))]
     "⟩"))
   []
   (Lean.cdot
    (Lean.cdotTk "·")
    (Tactic.tacticSeq
     (Tactic.tacticSeq1Indented
      [(Tactic.obtain
        "obtain"
        [(Tactic.rcasesPatMed
          [(Tactic.rcasesPat.tuple
            "⟨"
            [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `I)]) [])
             ","
             (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `hI)]) [])]
            "⟩")])]
        []
        [":=" [(Term.app `M.exists_isBasis [`X])]])
       []
       (Tactic.rwSeq
        "rw"
        (Tactic.optConfig [])
        (Tactic.rwRuleSeq "[" [(Tactic.rwRule [] `hI.eRk_eq_encard) "," (Tactic.rwRule [] `encard_le_one_iff_eq)] "]")
        [(Tactic.location "at" (Tactic.locationHyp [`h]))])
       []
       (Tactic.obtain
        "obtain"
        [(Tactic.rcasesPatMed
          [(Tactic.rcasesPat.paren
            "("
            (Tactic.rcasesPatLo
             (Tactic.rcasesPatMed
              [(Tactic.rcasesPat.one `rfl)
               "|"
               (Tactic.rcasesPat.tuple
                "⟨"
                [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `e)]) [])
                 ","
                 (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `rfl)]) [])]
                "⟩")])
             [])
            ")")])]
        []
        [":=" [`h]])
       []
       (Lean.cdot
        (Lean.cdotTk "·")
        (Tactic.tacticSeq
         (Tactic.tacticSeq1Indented
          [(Tactic.obtain
            "obtain"
            [(Tactic.rcasesPatMed
              [(Tactic.rcasesPat.tuple
                "⟨"
                [(Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `e)]) [])
                 ","
                 (Tactic.rcasesPatLo (Tactic.rcasesPatMed [(Tactic.rcasesPat.one `he)]) [])]
                "⟩")])]
            []
            [":=" [`M.ground_nonempty]])
           []
           (Tactic.exact
            "exact"
            (Term.anonymousCtor
             "⟨"
             [`e
              ","
              `he
              ","
              (Term.app
               `hI.subset_closure.trans
               [(Term.paren
                 (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                 (Term.paren
                  (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                  (Term.app
                   `M.closure_subset_closure
                   [(Term.paren
                     (Term.hygienicLParen "(" (hygieneInfo `[anonymous]))
                     (Term.app `empty_subset [(Term.hole "_")])
                     ")")])
                  ")")
                 ")")])]
             "⟩"))])))
       []
       (Tactic.exact
        "exact"
        (Term.anonymousCtor "⟨" [`e "," (Term.app `hI.indep.subset_ground [`rfl]) "," `hI.subset_closure] "⟩"))])))
   []
   (Tactic.refine
    "refine"
    (Term.app
     (Term.proj
      (Term.paren (Term.hygienicLParen "(" (hygieneInfo `[anonymous])) (Term.app `M.eRk_mono [`he]) ")")
      "."
      `trans)
     [(Term.syntheticHole "?" "_")]))
   []
   (Tactic.rwSeq
    "rw"
    (Tactic.optConfig [])
    (Tactic.rwRuleSeq
     "["
     [(Tactic.rwRule [] `eRk_closure_eq) "," (Tactic.rwRule ["←"] (Term.app `encard_singleton [`e]))]
     "]")
    [])
   []
   (Tactic.exact
    "exact"
    (Term.app
     `M.eRk_le_encard
     [(choice
       («term{_}» "{" [`e] "}")
       (Term.structInst
        "{"
        []
        (Term.structInstFields [(Term.structInstField (Term.structInstLVal `e []) [])])
        (Term.optEllipsis [])
        []
        "}"))]))]))

Goal state after: