Theorem: Matroid.Flat.rel_covByPartition_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✝ : α
hF : M.Flat F
e f : α
⊢ hF.covByPartition.Rel e f ↔ e ∈ M.E \ F ∧ f ∈ M.E \ F ∧ M.cl (insert e F) = M.cl (insert f F)
Tactic:
simp only [hF.covByPartition.rel_iff_partOf_eq_partOf', partOf_covByPartition_eq, mem_diff,
  exists_prop, exists_and_left, and_congr_right_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✝ : α
hF : M.Flat F
e f : α
⊢ e ∈ M.E ∧ e ∉ F →
    f ∈ M.E ∧ f ∉ F → (M.cl (insert e F) \ F = M.cl (insert f F) \ F ↔ M.cl (insert e F) = M.cl (insert f 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 f : α
⊢ e ∈ M.E ∧ e ∉ F →
    f ∈ M.E ∧ f ∉ F → (M.cl (insert e F) \ F = M.cl (insert f F) \ F ↔ M.cl (insert e F) = M.cl (insert f F))
Tactic:
refine fun _ _  ↦ ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
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 f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) \ F = M.cl (insert f F) \ F
⊢ M.cl (insert e F) = M.cl (insert f 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 f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) \ F = M.cl (insert f F) \ F
⊢ M.cl (insert e F) = M.cl (insert f F)
Tactic:
rw [← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert e F)),
  ← union_eq_self_of_subset_right (M.cl_subset_cl (subset_insert f F)), hF.cl,
  ← diff_union_self, h, diff_union_self]
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 f : α
x✝¹ : e ∈ M.E ∧ e ∉ F
x✝ : f ∈ M.E ∧ f ∉ F
h : M.cl (insert e F) = M.cl (insert f F)
⊢ M.cl (insert e F) \ F = M.cl (insert f F) \ F
Tactic:
rw [h]
State after:
no goals