Theorem: Matroid.flat_iff_forall_circuit (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 : autoParam (F ⊆ M.E) _auto✝
⊢ M.Flat F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
Tactic:
rw [flat_iff_cl_self]
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 : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F = F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → 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 : autoParam (F ⊆ M.E) _auto✝
⊢ M.cl F = F ↔ ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
Tactic:
refine' ⟨fun h C e hC heC hCF ↦ _, fun h ↦ _⟩
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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ F

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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
⊢ M.cl F = F

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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
⊢ M.cl F = F
Tactic:
refine' (M.subset_cl F hF).antisymm' (fun e heF ↦ by_contra fun he' ↦ _)
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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ 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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
⊢ False
Tactic:
obtain ⟨C, hC, heC, hCF⟩ := (mem_cl_iff_exists_circuit_of_not_mem he').mp heF
State after:
case refine'_2.intro.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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ False

State before:
case refine'_2.intro.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 : autoParam (F ⊆ M.E) _auto✝
h : ∀ (C : Set α) (e : α), M.Circuit C → e ∈ C → C ⊆ insert e F → e ∈ F
e : α
heF : e ∈ M.cl F
he' : e ∉ F
C : Set α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ False
Tactic:
exact he' (h C e hC heC hCF)
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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ F
Tactic:
rw [← h]
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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ M.cl F

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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ e ∈ M.cl F
Tactic:
refine' (M.cl_subset_cl _) (hC.subset_cl_diff_singleton e heC)
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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ C \ {e} ⊆ F

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 : autoParam (F ⊆ M.E) _auto✝
h : M.cl F = F
C : Set α
e : α
hC : M.Circuit C
heC : e ∈ C
hCF : C ⊆ insert e F
⊢ C \ {e} ⊆ F
Tactic:
rwa [diff_subset_iff, singleton_union]
State after:
no goals