Theorem: Matroid.ModularSet.Flat (Matroid/Modular.lean)

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : M.Simple
hF : M.ModularSet F
⊢ M.Flat F
Tactic:
by_contra h
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
⊢ False

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e f : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
⊢ False
Tactic:
obtain ⟨e, heF, he⟩ := exists_mem_cl_not_mem_of_not_flat h
State after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False

State before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : M.ModularSet F
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Tactic:
rw [modularSet_iff] at hF
State after:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False

State before:
case intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
⊢ False
Tactic:
obtain ⟨I, hI, hIF, hIe⟩ := hF (M.cl_flat {e})
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
⊢ False

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
⊢ False
Tactic:
have heM := M.cl_subset_ground F heF
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ False

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ False
Tactic:
have heI : e ∈ I := by
  rw [hI.inter_basis_cl_iff_subset_cl_inter, cl_singleton_eq,
    cl_eq_self_of_subset_singleton heM inter_subset_left] at hIe
  simpa using hIe
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ False

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ False
Tactic:
apply hI.not_mem_cl_diff_of_mem heI
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∈ M.cl (I \ {e})

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∈ M.cl (I \ {e})
Tactic:
apply mem_of_mem_of_subset <| M.cl_subset_cl_of_subset_cl hIF.subset_cl heF
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ M.cl (F ∩ I) ⊆ M.cl (I \ {e})

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ M.cl (F ∩ I) ⊆ M.cl (I \ {e})
Tactic:
apply M.cl_subset_cl
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ F ∩ I ⊆ I \ {e}

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ F ∩ I ⊆ I \ {e}
Tactic:
rw [subset_diff, and_iff_right inter_subset_right, disjoint_singleton_right]
State after:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∉ F ∩ I

State before:
case intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
heI : e ∈ I
⊢ e ∉ F ∩ I
Tactic:
exact fun he' ↦ he <| inter_subset_left he'
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : M.Basis (M.cl {e} ∩ I) (M.cl {e})
heM : e ∈ M.E
⊢ e ∈ I
Tactic:
rw [hI.inter_basis_cl_iff_subset_cl_inter, cl_singleton_eq,
  cl_eq_self_of_subset_singleton heM inter_subset_left] at hIe
State after:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : {e} ⊆ {e} ∩ I
heM : e ∈ M.E
⊢ e ∈ I

State before:
ι : Type u_1
α : Type u_2
M : Matroid α
B I✝ J X X' Y Y' F : Set α
Xs Ys Js Is : ι → Set α
i j : ι
e✝ f : α
inst✝ : M.Simple
hF : ∀ ⦃F_1 : Set α⦄, M.Flat F_1 → ∃ I, M.Indep I ∧ M.Basis (F ∩ I) F ∧ M.Basis (F_1 ∩ I) F_1
h : ¬M.Flat F
e : α
heF : e ∈ M.cl F
he : e ∉ F
I : Set α
hI : M.Indep I
hIF : M.Basis (F ∩ I) F
hIe : {e} ⊆ {e} ∩ I
heM : e ∈ M.E
⊢ e ∈ I
Tactic:
simpa using hIe
State after:
no goals