Theorem: Matroid.Indep.le_maxCommonInd (Matroid/Intersection.lean)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ I.ncard ≤ M₁.maxCommonInd M₂
Tactic:
rw [maxCommonInd, Nat.sSup_def, Nat.le_find_iff]
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ¬∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ m

case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∃ n, ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ n

State before:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∃ n, ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ n
Tactic:
refine ⟨M₁.E.ncard, ?_⟩
State after:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ M₁.E.ncard

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

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

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

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ¬∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ m
Tactic:
simp only [mem_setOf_eq, forall_exists_index, and_imp, not_forall, Classical.not_imp, not_le]
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ∃ x x_1, ∃ (_ : M₁.Indep x_1) (_ : M₂.Indep x_1) (_ : x_1.ncard = x), m < x

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ∃ x x_1, ∃ (_ : M₁.Indep x_1) (_ : M₂.Indep x_1) (_ : x_1.ncard = x), m < x
Tactic:
exact fun m hm ↦ ⟨_, I, hI₁, hI₂, rfl, hm⟩
State after:
no goals