rw [← diff_diff, diff_diff_right_self, r_eq_r_inter_ground, union_inter_distrib_right,
  disjoint_sdiff_left.inter_eq, empty_union, ← r_eq_r_inter_ground, hcard,
  restrict_r_eq _ (by simp [diff_subset]), restrict_ground_eq, M₂.r_eq_r_inter_ground,
  inter_diff_assoc, inter_comm]
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ I.ncard = M₁.r (M₂.E \ M₁.E ∪ X) + M₂.r (M₂.E \ (M₂.E \ M₁.E ∪ X))
no goals