internlm/Lean-Github huggingface dataset:
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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))
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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⟩
Proof 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 ∅)
Theorem: Matroid.exists_common_ind_aux
Proof 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]
Proof 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 ∅
Theorem: Matroid.exists_common_ind_aux
Proof 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]
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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]
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_aux
Proof 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]
Proof state after:
no goals