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

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I, X, -, hI₁, hI₂, hcard⟩ := exists_common_ind_aux M₁ (M₂ ↾ M₁.E) rfl
State after:
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 X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
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 X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine ⟨I, (M₂.E \ M₁.E) ∪ X, hI₁, hI₂.of_restrict, ?_⟩
State after:
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))

State before:
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))
Tactic:
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]
State after:
no goals

State before:
α : 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)
⊢ (M₂ ↾ M₁.E).E \ X ⊆ M₁.E
Tactic:
simp [diff_subset]
State after:
no goals