Theorem: Matroid.Flat.partOf_covByPartition_eq (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
e : α
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
by_cases he : e ∈ M.E \ F
State after:
case pos
α : 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
e : α
he : e ∈ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

case neg
α : 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
e : α
he : e ∉ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

State before:
case neg
α : 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
e : α
he : e ∉ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
have hrw : insert e F ∩ M.E = F := by
  refine subset_antisymm ?_ (subset_inter (subset_insert _ _) hF.subset_ground)
  rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
     (and_iff_left inter_subset_left)]
  rintro f ⟨rfl, hf⟩
  exact by_contra fun hfF ↦ he ⟨hf, hfF⟩
State after:
case neg
α : 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
e : α
he : e ∉ M.E \ F
hrw : insert e F ∩ M.E = F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

State before:
case neg
α : 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
e : α
he : e ∉ M.E \ F
hrw : insert e F ∩ M.E = F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
rw [← cl_inter_ground, hrw, hF.cl, diff_self, hF.covByPartition.partOf_eq_empty he]
State after:
no goals

State before:
case pos
α : 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
e : α
he : e ∈ M.E \ F
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
obtain ⟨F', hFF', hF'⟩ := hF.mem_covByPartition_iff.1 (hF.covByPartition.partOf_mem he)
State after:
case pos.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 : M.Flat F
e : α
he : e ∈ M.E \ F
F' : Set α
hFF' : F ⋖[M] F'
hF' : F' \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

State before:
case pos.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 : M.Flat F
e : α
he : e ∈ M.E \ F
F' : Set α
hFF' : F ⋖[M] F'
hF' : F' \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
obtain rfl := hFF'.cl_insert_eq (hF'.symm.subset <| hF.covByPartition.mem_partOf he)
State after:
case pos.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 : M.Flat F
e : α
he : e ∈ M.E \ F
hFF' : F ⋖[M] M.cl (insert e F)
hF' : M.cl (insert e F) \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F

State before:
case pos.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 : M.Flat F
e : α
he : e ∈ M.E \ F
hFF' : F ⋖[M] M.cl (insert e F)
hF' : M.cl (insert e F) \ F = hF.covByPartition.partOf e
⊢ hF.covByPartition.partOf e = M.cl (insert e F) \ F
Tactic:
exact hF'.symm
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 : α
hF : M.Flat F
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E = F
Tactic:
refine subset_antisymm ?_ (subset_inter (subset_insert _ _) hF.subset_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 : α
hF : M.Flat F
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.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
e : α
he : e ∉ M.E \ F
⊢ insert e F ∩ M.E ⊆ F
Tactic:
rw [← singleton_union, union_inter_distrib_right, union_subset_iff,
   (and_iff_left inter_subset_left)]
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
e : α
he : e ∉ M.E \ F
⊢ {e} ∩ M.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
e : α
he : e ∉ M.E \ F
⊢ {e} ∩ M.E ⊆ F
Tactic:
rintro f ⟨rfl, hf⟩
State after:
case 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 : M.Flat F
f : α
hf : f ∈ M.E
he : f ∉ M.E \ F
⊢ f ∈ F

State before:
case 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 : M.Flat F
f : α
hf : f ∈ M.E
he : f ∉ M.E \ F
⊢ f ∈ F
Tactic:
exact by_contra fun hfF ↦ he ⟨hf, hfF⟩
State after:
no goals