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