-- Mathlib/Data/Matroid/Restrict.lean
theorem Indep.augment (hI : M.Indep I) (hJ : M.Indep J) (hIJ : I.encard < J.encard) :
    ∃ e ∈ J \ I, M.Indep (insert e I)

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
⊢ False

Tactic:
obtain ⟨J', hJ', hJJ'⟩ := hJ.subset_isBasis_of_subset I.subset_union_right

Result:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
by_contra! he

Result:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ False

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
exact hIJ.not_le (encard_mono hJJ')

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ False

Tactic:
have hb : M.IsBasis I (I ∪ J) := by
  simp_rw [hI.isBasis_iff_forall_insert_dep subset_union_left, union_diff_left, mem_diff,
    and_imp, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground]
  exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩

Result:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
⊢ False

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ M.IsBasis I (I ∪ J)

Tactic:
simp_rw [hI.isBasis_iff_forall_insert_dep subset_union_left, union_diff_left, mem_diff,
  and_imp, dep_iff, insert_subset_iff, and_iff_left hI.subset_ground]

Result:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Proof state:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E

Tactic:
exact fun e heJ heI ↦ ⟨he e ⟨heJ, heI⟩, hJ.subset_ground heJ⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False

Tactic:
rw [← hJ'.encard_eq_encard hb] at hIJ

Result:
case intro.intro
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
hb : M.IsBasis I (I ∪ J)
J' : Set α
hIJ : J'.encard < J.encard
hJ' : M.IsBasis J' (I ∪ J)
hJJ' : J ⊆ J'
⊢ False