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

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.maxCommonInd M₂
Tactic:
refine Nat.sSup_mem (s := {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}) ⟨0, ∅, by simp⟩
  ⟨M₁.E.ncard, ?_⟩
State after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.E.ncard ∈ upperBounds {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.E.ncard ∈ upperBounds {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}
Tactic:
simp only [upperBounds, mem_setOf_eq, forall_exists_index, and_imp]
State after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∀ ⦃a : ℕ⦄ (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∀ ⦃a : ℕ⦄ (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
Tactic:
rintro _ I hI - rfl
State after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I : Set α
hI : M₁.Indep I
⊢ I.ncard ≤ M₁.E.ncard

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I : Set α
hI : M₁.Indep I
⊢ I.ncard ≤ M₁.E.ncard
Tactic:
exact ncard_le_ncard hI.subset_ground M₁.ground_finite
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.Indep ∅ ∧ M₂.Indep ∅ ∧ ∅.ncard = 0
Tactic:
simp
State after:
no goals