Theorem: Matroid.Flat.exists_unique_flat_of_not_mem (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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∃! F₁, e ∈ F₁ ∧ (F₀ ⋖[M] F₁)
Tactic:
simp_rw [hF₀.covBy_iff_eq_cl_insert]
State after:
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∃! F₁, e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)

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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∃! F₁, e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)
Tactic:
use M.cl (insert e F₀)
State after:
case h
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀)) ∧
    ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)

State before:
case h
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀)) ∧
    ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Tactic:
refine' ⟨_, _⟩
State after:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀))

case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)

State before:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∀ (y : Set α), (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) y → y = M.cl (insert e F₀)
Tactic:
simp only [exists_prop, and_imp, forall_exists_index]
State after:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∀ (y : Set α), e ∈ y → ∀ x ∈ M.E \ F₀, y = M.cl (insert x F₀) → y = M.cl (insert e F₀)

State before:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∀ (y : Set α), e ∈ y → ∀ x ∈ M.E \ F₀, y = M.cl (insert x F₀) → y = M.cl (insert e F₀)
Tactic:
rintro X heX f _ rfl
State after:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
f : α
a✝ : f ∈ M.E \ F₀
heX : e ∈ M.cl (insert f F₀)
⊢ M.cl (insert f F₀) = M.cl (insert e F₀)

State before:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
f : α
a✝ : f ∈ M.E \ F₀
heX : e ∈ M.cl (insert f F₀)
⊢ M.cl (insert f F₀) = M.cl (insert e F₀)
Tactic:
rw [hF₀.cl_insert_eq_cl_insert_of_mem ⟨heX, he.2⟩]
State after:
no goals

State before:
case h.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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ (fun F₁ => e ∈ F₁ ∧ ∃ e ∈ M.E \ F₀, F₁ = M.cl (insert e F₀)) (M.cl (insert e F₀))
Tactic:
constructor
State after:
case h.refine'_1.left
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ e ∈ M.cl (insert e F₀)

case h.refine'_1.right
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)

State before:
case h.refine'_1.right
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ ∃ e_1 ∈ M.E \ F₀, M.cl (insert e F₀) = M.cl (insert e_1 F₀)
Tactic:
use e, he
State after:
no goals

State before:
case h.refine'_1.left
α : 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₀ : M.Flat F₀
he : e ∈ M.E \ F₀
⊢ e ∈ M.cl (insert e F₀)
Tactic:
exact (M.inter_ground_subset_cl (insert e F₀)) ⟨mem_insert _ _, he.1⟩
State after:
no goals