Theorem: ClMatroid.matroidOnUniv_cl_eq (Matroid/Constructions/ClosureAxioms.lean)

State before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
obtain ⟨I, hI⟩ := (M.matroidOnUniv hM).exists_basis X (by simp [hM])
State after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
⊢ (M.matroidOnUniv hM).cl X = M.cl X

State before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
have hi := hI.indep
State after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.matroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X

State before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.matroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
simp [matroidOnUniv, M.clIndep_iff] at hi
State after:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X

State before:
case intro
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X = M.cl X
Tactic:
refine subset_antisymm ?_ ?_
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X ⊆ M.cl X

case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ M.cl X ⊆ (M.matroidOnUniv hM).cl X

State before:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ X ⊆ (M.matroidOnUniv hM).E
Tactic:
simp [hM]
State after:
α : Type u_1
I B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X : Set α
⊢ X ⊆ (M.indepMatroidOnUniv hM).E

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ (M.matroidOnUniv hM).cl X ⊆ M.cl X
Tactic:
simp_rw [← hI.cl_eq_cl, subset_def, hI.indep.mem_cl_iff']
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ (x : α), x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ (x : α), x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Tactic:
simp [M.clIndep_iff]
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ (M.indepMatroidOnUniv hM).E, ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ (M.indepMatroidOnUniv hM).E, ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I) → x ∈ M.cl X
Tactic:
refine fun e h ↦ by_contra fun heX ↦ ?_
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ False

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ False
Tactic:
have heI : e ∉ I := not_mem_subset (hI.subset.trans (M.subset_cl_self X (by simp [hM]))) heX
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
⊢ False

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
⊢ False
Tactic:
have heI' : e ∉ M.cl I := not_mem_subset (M.cl_subset_cl hI.subset) heX
State after:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
heI' : e ∉ M.cl I
⊢ False

State before:
case intro.refine_1
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
heI : e ∉ I
heI' : e ∉ M.cl I
⊢ False
Tactic:
obtain ⟨a, haI, ha⟩ := h
State after:
no goals

State before:
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
e : α
h : e ∈ (M.indepMatroidOnUniv hM).E
heX : ¬(((M.indepMatroidOnUniv hM).Indep (insert e I) → e ∈ I) → e ∈ M.cl X)
⊢ X ⊆ M.E
Tactic:
simp [hM]
State after:
no goals

State before:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ M.cl X ⊆ (M.matroidOnUniv hM).cl X
Tactic:
simp_rw [← hI.cl_eq_cl, subset_def, hI.indep.mem_cl_iff']
State after:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I)

State before:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.matroidOnUniv hM).E ∧ ((M.matroidOnUniv hM).Indep (insert x I) → x ∈ I)
Tactic:
simp only [matroidOnUniv_E, mem_univ, matroidOnUniv_Indep, true_and]
State after:
case intro.refine_2
α : Type u_1
I✝ B X✝ : Set α
M : ClMatroid α
hM : M.E = univ
X I : Set α
hI : (M.matroidOnUniv hM).Basis I X
hi : (M.indepMatroidOnUniv hM).Indep I
⊢ ∀ x ∈ M.cl X, x ∈ (M.indepMatroidOnUniv hM).E ∧ ((M.indepMatroidOnUniv hM).Indep (insert x I) → x ∈ I)