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
he : e ∈ M.E \ F
⊢ hF.covByPartition.Rel e f ↔ M.cl (insert e F) = M.cl (insert f F)
Tactic:
rw [hF.rel_covByPartition_iff, and_iff_right he, and_iff_right_iff_imp]
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
⊢ M.cl (insert e F) = M.cl (insert f F) → 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
he : e ∈ M.E \ F
⊢ M.cl (insert e F) = M.cl (insert f F) → f ∈ M.E \ F
Tactic:
refine fun hcl ↦ ⟨by_contra fun hf ↦ ?_, fun hfF ↦ ?_⟩
State after:
case 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
hcl : M.cl (insert e F) = M.cl (insert f F)
hf : f ∉ M.E
⊢ False

case 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
hcl : M.cl (insert e F) = M.cl (insert f F)
hfF : f ∈ F
⊢ False

State before:
case 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
hcl : M.cl (insert e F) = M.cl (insert f F)
hfF : f ∈ F
⊢ False
Tactic:
rw [insert_eq_of_mem hfF, hF.cl] at hcl
State after:
case 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
hcl : M.cl (insert e F) = F
hfF : f ∈ F
⊢ False

State before:
case 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
hcl : M.cl (insert e F) = F
hfF : f ∈ F
⊢ False
Tactic:
exact he.2 <| hcl.subset (M.mem_cl_of_mem (mem_insert e F))
State after:
no goals

State before:
case 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
hcl : M.cl (insert e F) = M.cl (insert f F)
hf : f ∉ M.E
⊢ False
Tactic:
rw [← M.cl_inter_ground (insert f F), insert_inter_of_not_mem hf,
  inter_eq_self_of_subset_left hF.subset_ground, hF.cl] at hcl
State after:
case 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
hcl : M.cl (insert e F) = F
hf : f ∉ M.E
⊢ False

State before:
case 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
hcl : M.cl (insert e F) = F
hf : f ∉ M.E
⊢ False
Tactic:
exact he.2 <| hcl.subset (M.mem_cl_of_mem (mem_insert e F))
State after:
no goals