Theorem: Matroid.Hyperplane.exchange_base_of_circuit (Matroid/Constructions/Relax.lean)

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
⊢ M.Base (insert f (H \ {e}))
Tactic:
have hcl := hH.cl_insert_eq hf.2 hf.1
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.cl (insert f H) = M.E
⊢ M.Base (insert f (H \ {e}))

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.cl (insert f H) = M.E
⊢ M.Base (insert f (H \ {e}))
Tactic:
rw [← cl_insert_cl_eq_cl_insert, ← hHc.cl_diff_singleton_eq_cl e, cl_insert_cl_eq_cl_insert,
  ← spanning_iff_cl (insert_subset hf.1 (diff_subset.trans hH.subset_ground))] at hcl
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Base (insert f (H \ {e}))

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Base (insert f (H \ {e}))
Tactic:
refine' hcl.base_of_indep _
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Indep (insert f (H \ {e}))

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ M.Indep (insert f (H \ {e}))
Tactic:
rw [← (hHc.diff_singleton_indep he).not_mem_cl_iff_of_not_mem (fun hf' ↦ hf.2 hf'.1),
  hHc.cl_diff_singleton_eq_cl e, hH.flat.cl]
State after:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ f ∉ H

State before:
α : Type u_1
M : Matroid α
E I H B X : Set α
e f : α
hH : M.Hyperplane H
hHc : M.Circuit H
he : e ∈ H
hf : f ∈ M.E \ H
hcl : M.Spanning (insert f (H \ {e}))
⊢ f ∉ H
Tactic:
exact hf.2
State after:
no goals