Theorem: Matroid.exists_common_ind_with_flat_left (Matroid/Intersection.lean)

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
have : M₂.Finite := ⟨hE.symm ▸ M₁.ground_finite⟩
State after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I,X, -, h1,h2, h⟩ := exists_common_ind_aux M₁ M₂ hE
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine ⟨I, _, M₁.cl_flat X, h1, h2, (h1.ncard_le_r_add_r h2 _).antisymm ?_⟩
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r (M₁.cl X) + M₂.r (M₂.E \ M₁.cl X) ≤ I.ncard

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r (M₁.cl X) + M₂.r (M₂.E \ M₁.cl X) ≤ I.ncard
Tactic:
rw [r_cl_eq, h, ← diff_inter_self_eq_diff (t := X), ← hE]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r X + M₂.r (M₁.E \ M₁.cl X) ≤ M₁.r X + M₂.r (M₁.E \ (X ∩ M₁.E))

State before:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r X + M₂.r (M₁.E \ M₁.cl X) ≤ M₁.r X + M₂.r (M₁.E \ (X ∩ M₁.E))
Tactic:
exact add_le_add_left (M₂.r_mono (diff_subset_diff_right <| inter_ground_subset_cl M₁ X)) _
State after:
no goals