Theorem: Matroid.exists_common_ind_aux (Matroid/Intersection.lean)

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
have _ : M₂.Finite := ⟨hE.symm ▸ M₁.ground_finite⟩
State after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
by_cases hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
State after:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ¬∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ¬∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
push_neg at hloop
State after:
case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∃ e ∈ M₁.E, ¬M₁.Loop e ∧ ¬M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∃ e ∈ M₁.E, ¬M₁.Loop e ∧ ¬M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨e, he, he₁, he₂⟩ := hloop
State after:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : ¬M₁.Loop e
he₂ : ¬M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : ¬M₁.Loop e
he₂ : ¬M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
rw [not_loop_iff] at he₁ he₂
State after:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
have : (M₁ ／ e).E.ncard < M₁.E.ncard := ncard_lt_ncard (by simpa) M₁.ground_finite
State after:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this : (M₁ ／ e).E.ncard < M₁.E.ncard
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this : (M₁ ／ e).E.ncard < M₁.E.ncard
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
have : (M₁ ＼ e).E.ncard < M₁.E.ncard := ncard_lt_ncard (by simpa) M₁.ground_finite
State after:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨Id, Xd, hXd, hId₁, hId₂, hId⟩ := exists_common_ind_aux (M₁ ＼ e) (M₂ ＼ e) (by simp [hE])
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨Ic, Xc, hXc, hIc₁, hIc₂, hIc⟩ := exists_common_ind_aux (M₁ ／ e) (M₂ ／ e) (by simp [hE])
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : (M₁ ／ e).Indep Ic
hIc₂ : (M₂ ／ e).Indep Ic
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : (M₁ ／ e).Indep Ic
hIc₂ : (M₂ ／ e).Indep Ic
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
rw [he₁.contract_indep_iff] at hIc₁
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : (M₂ ／ e).Indep Ic
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : (M₂ ／ e).Indep Ic
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
rw [he₂.contract_indep_iff] at hIc₂
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hXc : Xc ⊆ (M₁ ／ e).E
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
simp only [contract_elem, contract_ground, deleteElem, delete_ground,
  subset_diff_singleton_iff] at hXc hXd
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
by_contra! hcon
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard ≠ M₁.r X + M₂.r (M₂.E \ X)
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard ≠ M₁.r X + M₂.r (M₂.E \ X)
⊢ False
Tactic:
replace hcon :=
  show ∀ I X, X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard + 1 ≤ M₁.r X + M₂.r (M₂.E \ X) from
  fun I X hX h h' ↦ Nat.add_one_le_iff.2 <| (h.ncard_le_r_add_r h' X).lt_of_ne <| hcon I X hX h h'
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard + 1 ≤ M₁.r X + M₂.r (M₂.E \ X)
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard + 1 ≤ M₁.r X + M₂.r (M₂.E \ X)
⊢ False
Tactic:
have hcond := hcon Id (Xc ∩ Xd) (inter_subset_left.trans hXc.1) hId₁.of_delete hId₂.of_delete
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard + 1 ≤ M₁.r X + M₂.r (M₂.E \ X)
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard + 1 ≤ M₁.r X + M₂.r (M₂.E \ X)
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
⊢ False
Tactic:
replace hcon := hcon (insert e Ic) (insert e (Xc ∪ Xd))
  (insert_subset he₁.mem_ground (union_subset hXc.1 hXd.1)) hIc₁.2 hIc₂.2
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : (insert e Ic).ncard + 1 ≤ M₁.r (insert e (Xc ∪ Xd)) + M₂.r (M₂.E \ insert e (Xc ∪ Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : (insert e Ic).ncard + 1 ≤ M₁.r (insert e (Xc ∪ Xd)) + M₂.r (M₂.E \ insert e (Xc ∪ Xd))
⊢ False
Tactic:
rw [ncard_insert_of_not_mem hIc₁.1 (hIc₁.2.subset (subset_insert _ _)).finite,
  ← insert_union] at hcon
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
⊢ False
Tactic:
have hsm := M₁.r_submod (insert e Xc) Xd
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (insert e Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (insert e Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
⊢ False
Tactic:
rw [insert_inter_of_not_mem hXd.2] at hsm
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
⊢ False
Tactic:
have hsm2 := M₂.r_submod (M₂.E \ Xc) ((M₂.E \ insert e Xd))
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
hsm2 :
  M₂.r (M₂.E \ Xc ∩ (M₂.E \ insert e Xd)) + M₂.r (M₂.E \ Xc ∪ M₂.E \ insert e Xd) ≤
    M₂.r (M₂.E \ Xc) + M₂.r (M₂.E \ insert e Xd)
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
hsm2 :
  M₂.r (M₂.E \ Xc ∩ (M₂.E \ insert e Xd)) + M₂.r (M₂.E \ Xc ∪ M₂.E \ insert e Xd) ≤
    M₂.r (M₂.E \ Xc) + M₂.r (M₂.E \ insert e Xd)
⊢ False
Tactic:
simp_rw [diff_eq, ← inter_inter_distrib_left, ← inter_union_distrib_left, ← compl_inter,
  ← compl_union, union_insert, ← insert_union, inter_comm Xc, insert_inter_of_not_mem hXc.2,
  inter_comm Xd, ← diff_eq] at hsm2
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
hsm2 : M₂.r (M₂.E \ (insert e Xc ∪ Xd)) + M₂.r (M₂.E \ (Xc ∩ Xd)) ≤ M₂.r (M₂.E \ Xc) + M₂.r (M₂.E \ insert e Xd)
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hIc : Ic.ncard = (M₁ ／ e).r Xc + (M₂ ／ e).r ((M₂ ／ e).E \ Xc)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcond : Id.ncard + 1 ≤ M₁.r (Xc ∩ Xd) + M₂.r (M₂.E \ (Xc ∩ Xd))
hcon : Ic.ncard + 1 + 1 ≤ M₁.r (insert e Xc ∪ Xd) + M₂.r (M₂.E \ (insert e Xc ∪ Xd))
hsm : M₁.r (Xc ∩ Xd) + M₁.r (insert e Xc ∪ Xd) ≤ M₁.r (insert e Xc) + M₁.r Xd
hsm2 : M₂.r (M₂.E \ (insert e Xc ∪ Xd)) + M₂.r (M₂.E \ (Xc ∩ Xd)) ≤ M₂.r (M₂.E \ Xc) + M₂.r (M₂.E \ insert e Xd)
⊢ False
Tactic:
zify at hcon hcond hId hIc hsm hsm2
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑((M₁ ＼ e).r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑((M₁ ／ e).r Xc) + ↑((M₂ ／ e).r ((M₂ ／ e).E \ Xc))
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑((M₁ ＼ e).r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑((M₁ ／ e).r Xc) + ↑((M₂ ／ e).r ((M₂ ／ e).E \ Xc))
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False
Tactic:
rw [he₂.contract_r_cast_int_eq, he₁.contract_r_cast_int_eq, contract_elem, contract_ground,
  diff_diff_comm, insert_diff_singleton,
    insert_eq_of_mem (show e ∈ M₂.E \ Xc from ⟨he₂.mem_ground, hXc.2⟩)] at hIc
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑((M₁ ＼ e).r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑((M₁ ＼ e).r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False
Tactic:
rw [delete_elem_r_eq _ hXd.2, delete_elem_r_eq _ (by simp), deleteElem, delete_ground,
  diff_diff_comm, diff_diff, union_singleton] at hId
State after:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑(M₁.r Xd) + ↑(M₂.r (M₂.E \ insert e Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False

State before:
case neg.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑(M₁.r Xd) + ↑(M₂.r (M₂.E \ insert e Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
suffices 0 = M₂.r (M₂.E \ M₁.cl ∅) from ⟨∅, M₁.cl ∅, cl_subset_ground _ _, by simpa⟩
State after:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ 0 = M₂.r (M₂.E \ M₁.cl ∅)

State before:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ 0 = M₂.r (M₂.E \ M₁.cl ∅)
Tactic:
rw [eq_comm, r_eq_zero_iff diff_subset, diff_subset_iff, ← hE]
State after:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ M₁.E ⊆ M₁.cl ∅ ∪ M₂.cl ∅

State before:
case pos
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
⊢ M₁.E ⊆ M₁.cl ∅ ∪ M₂.cl ∅
Tactic:
simpa [subset_def]
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
hloop : ∀ e ∈ M₁.E, M₁.Loop e ∨ M₂.Loop e
this : 0 = M₂.r (M₂.E \ M₁.cl ∅)
⊢ M₁.Indep ∅ ∧ M₂.Indep ∅ ∧ ∅.ncard = M₁.r (M₁.cl ∅) + M₂.r (M₂.E \ M₁.cl ∅)
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
⊢ (M₁ ／ e).E ⊂ M₁.E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this : (M₁ ／ e).E.ncard < M₁.E.ncard
⊢ (M₁ ＼ e).E ⊂ M₁.E
Tactic:
simpa
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
⊢ (M₁ ＼ e).E = (M₂ ＼ e).E
Tactic:
simp [hE]
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hXd : Xd ⊆ (M₁ ＼ e).E
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
hId : Id.ncard = (M₁ ＼ e).r Xd + (M₂ ＼ e).r ((M₂ ＼ e).E \ Xd)
⊢ (M₁ ／ e).E = (M₂ ／ e).E
Tactic:
simp [hE]
State after:
no goals

State before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
hE : M₁.E = M₂.E
x✝ : M₂.Finite
e : α
he : e ∈ M₁.E
he₁ : M₁.Nonloop e
he₂ : M₂.Nonloop e
this✝ : (M₁ ／ e).E.ncard < M₁.E.ncard
this : (M₁ ＼ e).E.ncard < M₁.E.ncard
Id Xd : Set α
hId₁ : (M₁ ＼ e).Indep Id
hId₂ : (M₂ ＼ e).Indep Id
Ic Xc : Set α
hIc₁ : e ∉ Ic ∧ M₁.Indep (insert e Ic)
hIc₂ : e ∉ Ic ∧ M₂.Indep (insert e Ic)
hXc : Xc ⊆ M₁.E ∧ e ∉ Xc
hXd : Xd ⊆ M₁.E ∧ e ∉ Xd
hcon : ↑Ic.ncard + 1 + 1 ≤ ↑(M₁.r (insert e Xc ∪ Xd)) + ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd)))
hcond : ↑Id.ncard + 1 ≤ ↑(M₁.r (Xc ∩ Xd)) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd)))
hId : ↑Id.ncard = ↑(M₁.r Xd) + ↑((M₂ ＼ e).r ((M₂ ＼ e).E \ Xd))
hIc : ↑Ic.ncard = ↑(M₁.r (insert e Xc)) - 1 + (↑(M₂.r (M₂.E \ Xc)) - 1)
hsm : ↑(M₁.r (Xc ∩ Xd)) + ↑(M₁.r (insert e Xc ∪ Xd)) ≤ ↑(M₁.r (insert e Xc)) + ↑(M₁.r Xd)
hsm2 :
  ↑(M₂.r (M₂.E \ (insert e Xc ∪ Xd))) + ↑(M₂.r (M₂.E \ (Xc ∩ Xd))) ≤ ↑(M₂.r (M₂.E \ Xc)) + ↑(M₂.r (M₂.E \ insert e Xd))
⊢ e ∉ (M₂ ＼ e).E \ Xd
Tactic:
simp
State after:
no goals