Theorem: Matroid.flat_iff_ssubset_cl_insert_forall (Matroid/Flat.lean)

State before:
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
Tactic:
refine' ⟨fun h e he ↦ (M.cl_subset_cl (subset_insert _ _)).ssubset_of_ne _, fun h ↦ _⟩
State after:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ M.cl F ≠ M.cl (insert e F)

case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.Flat F

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.Flat F
Tactic:
rw [flat_iff_cl_self]
State after:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.cl F = F

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
⊢ M.cl F = F
Tactic:
by_contra h'
State after:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
⊢ False

State before:
case refine'_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
⊢ False
Tactic:
obtain ⟨e, he', heF⟩ := exists_of_ssubset (ssubset_of_ne_of_subset (Ne.symm h') (M.subset_cl F))
State after:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
⊢ False

State before:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
⊢ False
Tactic:
have h'' := h e ⟨(M.cl_subset_ground F) he', heF⟩
State after:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl (insert e F)
⊢ False

State before:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl (insert e F)
⊢ False
Tactic:
rw [← M.cl_insert_cl_eq_cl_insert e F, insert_eq_of_mem he', M.cl_cl] at h''
State after:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl F
⊢ False

State before:
case refine'_2.intro.intro
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : ∀ e ∈ M.E \ F, M.cl F ⊂ M.cl (insert e F)
h' : ¬M.cl F = F
e : α
he' : e ∈ M.cl F
heF : e ∉ F
h'' : M.cl F ⊂ M.cl F
⊢ False
Tactic:
exact h''.ne rfl
State after:
no goals

State before:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ M.cl F ≠ M.cl (insert e F)
Tactic:
rw [h.cl]
State after:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ F ≠ M.cl (insert e F)

State before:
case refine'_1
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hF : autoParam (F ⊆ M.E) _auto✝
h : M.Flat F
e : α
he : e ∈ M.E \ F
⊢ F ≠ M.cl (insert e F)
Tactic:
exact fun h' ↦ mt ((Set.ext_iff.mp h') e).mpr (not_mem_of_mem_diff he)
  ((M.subset_cl _ (insert_subset he.1 hF)) (mem_insert _ _))
State after:
no goals