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

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ I.ncard ≤ M₁.r A + M₂.r (M₂.E \ A)
Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard I A hI₂.finite, ← (hI₁.inter_right A).r,
  ← (hI₂.diff A).r]
State after:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ M₁.r (I ∩ A) + M₂.r (I \ A) ≤ M₁.r A + M₂.r (M₂.E \ A)

State before:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ M₁.r (I ∩ A) + M₂.r (I \ A) ≤ M₁.r A + M₂.r (M₂.E \ A)
Tactic:
exact add_le_add (M₁.r_mono inter_subset_right)
  (M₂.r_mono (diff_subset_diff_left hI₂.subset_ground))
State after:
no goals