Theorem: Matroid.flat_restrict_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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).Flat F ↔ ∃ F', M.Flat F' ∧ F = F' ∩ R
Tactic:
refine ⟨fun h ↦ ⟨M.cl F, M.cl_flat F, ?_⟩, ?_⟩
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ F = M.cl F ∩ R

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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (∃ F', M.Flat F' ∧ F = F' ∩ R) → (M ↾ R).Flat 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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (∃ F', M.Flat F' ∧ F = F' ∩ R) → (M ↾ R).Flat F
Tactic:
rintro ⟨F, hF, rfl⟩
State after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).Flat (F ∩ R)

State before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).Flat (F ∩ R)
Tactic:
rw [flat_iff_subset_cl_self]
State after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R

State before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
Tactic:
suffices M.cl (F ∩ R) ∩ R ⊆ F by simpa [inter_assoc, diff_eq_empty.2 hR]
State after:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ M.cl (F ∩ R) ∩ R ⊆ F

State before:
case refine_2.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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
⊢ M.cl (F ∩ R) ∩ R ⊆ F
Tactic:
exact inter_subset_left.trans (hF.cl_subset_of_subset inter_subset_left)
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ F = M.cl F ∩ R
Tactic:
nth_rw 1 [← h.cl]
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ (M ↾ R).cl F = M.cl F ∩ R

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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
⊢ (M ↾ R).cl F = M.cl F ∩ R
Tactic:
have hFR : F ⊆ R := h.subset_ground
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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
hFR : F ⊆ R
⊢ (M ↾ R).cl F = M.cl F ∩ R

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 : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
h : (M ↾ R).Flat F
hFR : F ⊆ R
⊢ (M ↾ R).cl F = M.cl F ∩ R
Tactic:
simp [inter_eq_self_of_subset_left hFR, diff_subset, diff_eq_empty.2 hR]
State after:
no goals

State before:
α : Type u_1
M : Matroid α
I X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e f : α
R : Set α
hR : autoParam (R ⊆ M.E) _auto✝
F : Set α
hF : M.Flat F
this : M.cl (F ∩ R) ∩ R ⊆ F
⊢ (M ↾ R).cl (F ∩ R) ⊆ F ∩ R
Tactic:
simpa [inter_assoc, diff_eq_empty.2 hR]
State after:
no goals