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