Theorem: Matroid.er_augment (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 : α
h : M.er X < M.er Z
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis' X
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_basis'_of_subset (hI.subset.trans subset_union_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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have hlt := h.trans_le (M.er_mono (subset_union_right (s := X)))
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
hlt : M.er X < M.er (X ∪ Z)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ ?m.32367)
hIJ : I ⊆ J
hlt : M.er X < M.er (X ∪ Z)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
rw [hI.er_eq_encard, hJ.er_eq_encard] at hlt
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
obtain ⟨e, heJ, heI⟩ := exists_of_ssubset (hIJ.ssubset_of_ne (by rintro rfl; exact hlt.ne rfl))
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have heIi : M.Indep (insert e I) := hJ.indep.subset (insert_subset heJ hIJ)
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
have heX : e ∉ X := fun h ↦
  heI (hI.basis_inter_ground.mem_of_insert_indep ⟨h, hJ.indep.subset_ground heJ⟩ heIi)
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ ∃ z ∈ Z \ X, M.er (insert z X) = M.er X + 1
Tactic:
refine ⟨e, ⟨Or.elim (hJ.subset heJ) (False.elim ∘ heX) id, heX⟩, ?_⟩
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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ M.er (insert e X) = M.er X + 1

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 : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
e : α
heJ : e ∈ J
heI : e ∉ I
heIi : M.Indep (insert e I)
heX : e ∉ X
⊢ M.er (insert e X) = M.er X + 1
Tactic:
rw [← hI.er_eq_er_insert, hI.er_eq_encard, heIi.er, encard_insert_of_not_mem heI]
State after:
no goals

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
J : Set α
hJ : M.Basis' J (X ∪ Z)
hIJ : I ⊆ J
hlt : I.encard < J.encard
⊢ I ≠ J
Tactic:
rintro rfl
State after:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
hJ : M.Basis' I (X ∪ Z)
hIJ : I ⊆ I
hlt : I.encard < I.encard
⊢ False

State before:
α : Type u_1
ι : Type u_2
M N : Matroid α
I✝ B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
h : M.er X < M.er Z
I : Set α
hI : M.Basis' I X
hJ : M.Basis' I (X ∪ Z)
hIJ : I ⊆ I
hlt : I.encard < I.encard
⊢ False
Tactic:
exact hlt.ne rfl
State after:
no goals