Theorem: Matroid.Indep.basis'_basis'_of_ncard_eq (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
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.Basis' (I ∩ A) A ∧ M₂.Basis' (I \ A) (M₂.E \ A)
Tactic:
rw [basis'_iff_indep_encard_eq_of_finite (hI₁.finite.subset inter_subset_left),
  and_iff_right inter_subset_right, and_iff_right (hI₁.inter_right A),
  basis'_iff_indep_encard_eq_of_finite (hI₁.finite.diff _), and_iff_right (hI₂.diff A),
  and_iff_right (diff_subset_diff_left hI₂.subset_ground), ← (hI₂.diff A).er,
  er_eq_er_iff, ← (hI₁.inter_right A).er, er_eq_er_iff]
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
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ 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
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ 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] at h
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
h : M₁.r A + M₂.r (M₂.E \ A) ≤ M₁.r (I ∩ A) + M₂.r (I \ A)
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ 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
h : M₁.r A + M₂.r (M₂.E \ A) ≤ M₁.r (I ∩ A) + M₂.r (I \ A)
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ A) = M₂.r (M₂.E \ A)
Tactic:
constructor <;>
linarith [M₁.r_mono (show I ∩ A ⊆ A from inter_subset_right),
  M₂.r_mono (show I \ A ⊆ M₂.E \ A from diff_subset_diff_left hI₂.subset_ground)]
State after:
no goals