Theorem: Matroid.er_eq_of_er_insert_le_forall (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 : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
⊢ M.er X = M.er Y
Tactic:
refine (M.er_mono hXY).eq_of_not_lt (fun hlt ↦ ?_)
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
⊢ False

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
⊢ False
Tactic:
obtain ⟨e, he, hins⟩ := er_augment hlt
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
⊢ False

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hY : ∀ e ∈ Y \ X, M.er (insert e X) ≤ M.er X
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
⊢ False
Tactic:
specialize hY e he
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : M.er (insert e X) ≤ M.er X
⊢ False

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : M.er (insert e X) ≤ M.er X
⊢ False
Tactic:
rw [← add_zero (M.er X), hins,
  WithTop.add_le_add_iff_left (fun htop ↦ not_top_lt (htop ▸ hlt))] at hY
State after:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : 1 ≤ 0
⊢ False

State before:
case intro.intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e✝ f : α
hXY : X ⊆ Y
hlt : M.er X < M.er Y
e : α
he : e ∈ Y \ X
hins : M.er (insert e X) = M.er X + 1
hY : 1 ≤ 0
⊢ False
Tactic:
simp at hY
State after:
no goals