Theorem: Matroid.flat_delete_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 : α
D : Set α
⊢ (M ＼ D).Flat F ↔ ∃ F', M.Flat F' ∧ F = F' \ D
Tactic:
simp_rw [delete_eq_restrict, flat_restrict_iff diff_subset, ← inter_diff_assoc]
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 : α
D : Set α
⊢ (∃ F', M.Flat F' ∧ F = (F' ∩ M.E) \ D) ↔ ∃ F', M.Flat F' ∧ F = F' \ D

State before:
case mpr
α : 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 : α
D : Set α
⊢ (∃ F', M.Flat F' ∧ F = F' \ D) → ∃ F', M.Flat F' ∧ F = (F' ∩ M.E) \ D
Tactic:
rintro ⟨F, hF, rfl⟩
State after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
D F : Set α
hF : M.Flat F
⊢ ∃ F', M.Flat F' ∧ F \ D = (F' ∩ M.E) \ D

State before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
D F : Set α
hF : M.Flat F
⊢ ∃ F', M.Flat F' ∧ F \ D = (F' ∩ M.E) \ D
Tactic:
refine ⟨F, hF, ?_⟩
State after:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
D F : Set α
hF : M.Flat F
⊢ F \ D = (F ∩ M.E) \ D

State before:
case mpr.intro.intro
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
D F : Set α
hF : M.Flat F
⊢ F \ D = (F ∩ M.E) \ D
Tactic:
rw [inter_eq_self_of_subset_left hF.subset_ground]
State after:
no goals