Theorem: Matroid.rFin.submod (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 : α
hX : M.rFin X
hY : M.rFin Y
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
obtain ⟨c, h_eq⟩ := le_iff_exists_add.1 <| M.er_inter_add_er_union_le_er_add_er 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 : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r 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 : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
obtain (rfl | hc) := eq_or_ne c ⊤
State after:
case intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

State before:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
have hi : M.rFin (X ∩ Y) := hX.subset inter_subset_left
State after:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

State before:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
have hu : M.rFin (X ∪ Y) := hX.union hY
State after:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

State before:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
rw [← ge_iff_le, r,r, ge_iff_le, ← toNat_add hX.ne hY.ne, h_eq, toNat_add _ hc,
  toNat_add hi.ne hu.ne, ← r, ← r]
State after:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r (X ∩ Y) + M.r (X ∪ Y) + toNat c

α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≠ ⊤

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.er (X ∩ Y) + M.er (X ∪ Y) ≠ ⊤
Tactic:
rw [Ne, WithTop.add_eq_top, not_or]
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ ¬M.er (X ∩ Y) = ⊤ ∧ ¬M.er (X ∪ Y) = ⊤

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ ¬M.er (X ∩ Y) = ⊤ ∧ ¬M.er (X ∪ Y) = ⊤
Tactic:
exact ⟨hi.ne, hu.ne⟩
State after:
no goals

State before:
case intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
rw [add_top, WithTop.add_eq_top] at h_eq
State after:
case intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
h_eq : M.er X = ⊤ ∨ M.er Y = ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y

State before:
case intro.inl
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
h_eq : M.er X = ⊤ ∨ M.er Y = ⊤
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r X + M.r Y
Tactic:
simp [hX.ne, hY.ne] at h_eq
State after:
no goals

State before:
case intro.inr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hX : M.rFin X
hY : M.rFin Y
c : ℕ∞
h_eq : M.er X + M.er Y = M.er (X ∩ Y) + M.er (X ∪ Y) + c
hc : c ≠ ⊤
hi : M.rFin (X ∩ Y)
hu : M.rFin (X ∪ Y)
⊢ M.r (X ∩ Y) + M.r (X ∪ Y) ≤ M.r (X ∩ Y) + M.r (X ∪ Y) + toNat c
Tactic:
apply Nat.le_add_right
State after:
no goals