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

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ M₁.maxCommonInd M₂ = ⨅ X, M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine le_antisymm (le_ciInf fun X ↦ ?_) ?_
State after:
case refine_1
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X : Set α
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)

case refine_2
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂

State before:
case refine_2
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Tactic:
obtain ⟨I, X, hI₁, hI₂, h⟩ := exists_common_ind M₁ M₂
State after:
case refine_2.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂

State before:
case refine_2.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Tactic:
exact (ciInf_le ⟨0, by simp [lowerBounds]⟩ X).trans (h.symm.le.trans (hI₁.le_maxCommonInd hI₂))
State after:
no goals

State before:
case refine_1
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X : Set α
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I, hI₁, hI₂, hI⟩ := maxCommonInd_exists M₁ M₂
State after:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)

State before:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
rw [← hI]
State after:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ I.ncard ≤ M₁.r X + M₂.r (M₂.E \ X)

State before:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ I.ncard ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
exact hI₁.ncard_le_r_add_r hI₂ X
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ 0 ∈ lowerBounds (range fun X => M₁.r X + M₂.r (M₂.E \ X))
Tactic:
simp [lowerBounds]
State after:
no goals