Theorem: Matroid.er_inter_add_er_union_le_er_add_er (Matroid/Rank.lean)

State before:
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y : Set α
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨Ii, hIi⟩ := M.exists_basis' (X ∩ Y)
State after:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y

State before:
case intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨IX, hIX, hIX'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_left)
State after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y

State before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
obtain ⟨IY, hIY, hIY'⟩ :=
  hIi.indep.subset_basis'_of_subset (hIi.subset.trans inter_subset_right)
State after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y

State before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≤ M.er X + M.er Y
Tactic:
rw [← hIX.er_eq_er_union, union_comm, ← hIY.er_eq_er_union, ← hIi.encard, ← hIX.encard,
  ← hIY.encard, union_comm, ← encard_union_add_encard_inter, add_comm]
State after:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard

State before:
case intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
M✝ N : Matroid α
I B X✝ X' Y✝ Y' Z R : Set α
n : ℕ∞
e f : α
M : Matroid α
X Y Ii : Set α
hIi : M.Basis' Ii (X ∩ Y)
IX : Set α
hIX : M.Basis' IX X
hIX' : Ii ⊆ IX
IY : Set α
hIY : M.Basis' IY Y
hIY' : Ii ⊆ IY
⊢ M.er (IX ∪ IY) + Ii.encard ≤ (IX ∪ IY).encard + (IX ∩ IY).encard
Tactic:
exact add_le_add (er_le_encard _ _) (encard_mono (subset_inter hIX' hIY'))
State after:
no goals