Theorem: Matroid.cl_covBy_cl_iff (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 : α
⊢ M.cl X ⋖[M] M.cl Y ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
rw [cl_covBy_iff]
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 : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y

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 : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
refine ⟨fun ⟨e, he, hYX⟩ ↦ ?_, fun ⟨e, he, _, heX, h_eq⟩ ↦ ⟨e, ⟨he, heX⟩, h_eq.symm⟩ ⟩
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
⊢ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
⊢ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
Tactic:
by_contra! hcon
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ False

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ False
Tactic:
have hY : Y ∩ M.E ⊆ M.cl X := by
  refine fun f hf ↦ by_contra fun hfX ↦ hcon f hf.2 hf.1 hfX ?_
  rw [hYX]
  apply cl_insert_eq_cl_insert_of_mem ⟨?_, hfX⟩
  rw [← hYX, ← cl_inter_ground]
  exact M.subset_cl _ (by aesop_mat) hf
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : Y ∩ M.E ⊆ M.cl X
⊢ False

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : Y ∩ M.E ⊆ M.cl X
⊢ False
Tactic:
replace hY := M.cl_subset_cl_of_subset_cl hY
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (Y ∩ M.E) ⊆ M.cl X
⊢ False

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (Y ∩ M.E) ⊆ M.cl X
⊢ False
Tactic:
rw [cl_inter_ground, hYX] at hY
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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (insert e X) ⊆ M.cl X
⊢ False

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
hY : M.cl (insert e X) ⊆ M.cl X
⊢ False
Tactic:
exact he.2 <| hY (M.mem_cl_of_mem' (mem_insert _ _) he.1)
State after:
no goals

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 : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
⊢ Y ∩ M.E ⊆ M.cl X
Tactic:
refine fun f hf ↦ by_contra fun hfX ↦ hcon f hf.2 hf.1 hfX ?_
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl Y

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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl Y
Tactic:
rw [hYX]
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl (insert e X)

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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ M.cl (insert f X) = M.cl (insert e X)
Tactic:
apply cl_insert_eq_cl_insert_of_mem ⟨?_, hfX⟩
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (insert e X)

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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (insert e X)
Tactic:
rw [← hYX, ← cl_inter_ground]
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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (Y ∩ M.E)

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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ f ∈ M.cl (Y ∩ M.E)
Tactic:
exact M.subset_cl _ (by aesop_mat) hf
State after:
no goals

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✝ : α
x✝ : ∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)
e : α
he : e ∈ M.E \ M.cl X
hYX : M.cl Y = M.cl (insert e X)
hcon : ∀ e ∈ M.E, e ∈ Y → e ∉ M.cl X → M.cl (insert e X) ≠ M.cl Y
f : α
hf : f ∈ Y ∩ M.E
hfX : f ∉ M.cl X
⊢ Y ∩ M.E ⊆ M.E
Tactic:
aesop_mat
State after:
no goals