internlm/Lean-Github huggingface dataset:
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)
Tactic:
suffices : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r),
  M.cl (⋂ (o' : Ordinal.{u}) (ho' : o' < o), Xs (Ordinal.enum r o' (ho'.trans ho))) = {k}
Proof state after:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
this : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
this : ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
⊢ ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r✝), P (range fun p => Ordinal.enum r✝ ↑p ⋯)

case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
Tactic:
sorry
Proof state after:
case this
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r✝ : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
r : ι → ι → Prop := WellOrderingRel
⊢ ∀ (o : Ordinal.{u}) (ho : o < Ordinal.type r), M.cl (⋂ o', ⋂ (ho' : o' < o), Xs (Ordinal.enum r o' ⋯)) = {k}
Theorem: cl_iInter_eq_iInter_cl
Proof state before:
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ M.cl (⋂ i, Xs i) = {k}
Tactic:
convert hwin (Ordinal.type r) rfl.le
Proof state after:
case h.e'_2.h.e'_3.h.e'_3.h
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
x✝ : ι
⊢ Xs x✝ = ⋂ (_ : x✝ ∈ range fun p => Ordinal.enum r ↑p ⋯), Xs x✝

case h.e'_3
α : Type u_1
ι : Type u
M : Matroid α
Xs : ι → Set α
k : α
h : ∀ ⦃i j : ι⦄, Xs i ⊆ Xs j ∨ Xs j ⊆ Xs i
r : ι → ι → Prop := WellOrderingRel
P : Set ι → Prop := fun I => M.cl (⋂ i ∈ I, Xs i) = ⋂ i ∈ I, M.cl (Xs i)
hwin : ∀ (o : Ordinal.{u}) (ho : o ≤ Ordinal.type r), P (range fun p => Ordinal.enum r ↑p ⋯)
⊢ {k} = ⋂ i ∈ range fun p => Ordinal.enum r ↑p ⋯, M.cl (Xs i)
Theorem: Matroid.Indep.ncard_le_r_add_r
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ I.ncard ≤ M₁.r A + M₂.r (M₂.E \ A)
Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard I A hI₂.finite, ← (hI₁.inter_right A).r,
  ← (hI₂.diff A).r]
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ M₁.r (I ∩ A) + M₂.r (I \ A) ≤ M₁.r A + M₂.r (M₂.E \ A)
Theorem: Matroid.Indep.ncard_le_r_add_r
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A✝ I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
A : Set α
⊢ M₁.r (I ∩ A) + M₂.r (I \ A) ≤ M₁.r A + M₂.r (M₂.E \ A)
Tactic:
exact add_le_add (M₁.r_mono inter_subset_right)
  (M₂.r_mono (diff_subset_diff_left hI₂.subset_ground))
Proof state after:
no goals
Theorem: Matroid.Indep.basis'_basis'_of_ncard_eq
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.Basis' (I ∩ A) A ∧ M₂.Basis' (I \ A) (M₂.E \ A)
Tactic:
rw [basis'_iff_indep_encard_eq_of_finite (hI₁.finite.subset inter_subset_left),
  and_iff_right inter_subset_right, and_iff_right (hI₁.inter_right A),
  basis'_iff_indep_encard_eq_of_finite (hI₁.finite.diff _), and_iff_right (hI₂.diff A),
  and_iff_right (diff_subset_diff_left hI₂.subset_ground), ← (hI₂.diff A).er,
  er_eq_er_iff, ← (hI₁.inter_right A).er, er_eq_er_iff]
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ A) = M₂.r (M₂.E \ A)
Theorem: Matroid.Indep.basis'_basis'_of_ncard_eq
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : M₁.r A + M₂.r (M₂.E \ A) ≤ I.ncard
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ A) = M₂.r (M₂.E \ A)
Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard I A hI₂.finite, ← (hI₁.inter_right A).r,
  ← (hI₂.diff A).r] at h
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : M₁.r A + M₂.r (M₂.E \ A) ≤ M₁.r (I ∩ A) + M₂.r (I \ A)
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ A) = M₂.r (M₂.E \ A)
Theorem: Matroid.Indep.basis'_basis'_of_ncard_eq
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝¹ : M₁.FiniteRk
inst✝ : M₂.FiniteRk
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : M₁.r A + M₂.r (M₂.E \ A) ≤ M₁.r (I ∩ A) + M₂.r (I \ A)
⊢ M₁.r (I ∩ A) = M₁.r A ∧ M₂.r (I \ A) = M₂.r (M₂.E \ A)
Tactic:
constructor <;>
linarith [M₁.r_mono (show I ∩ A ⊆ A from inter_subset_right),
  M₂.r_mono (show I \ A ⊆ M₂.E \ A from diff_subset_diff_left hI₂.subset_ground)]
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
⊢ ∃ 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⟩
Proof 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)
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
⊢ ∃ 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
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
⊢ ∃ 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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₂
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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])
Proof 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)
Theorem: Matroid.exists_common_ind_aux
Proof 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])
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 α
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)
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 α
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₁
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 α
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)
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 α
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₂
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 α
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)
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 α
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
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
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
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
⊢ ∃ I, ∃ X ⊆ M₁.E, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
by_contra! 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
hcon : ∀ (I X : Set α), X ⊆ M₁.E → M₁.Indep I → M₂.Indep I → I.ncard ≠ M₁.r X + M₂.r (M₂.E \ X)
⊢ 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
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'
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
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
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)
⊢ False
Tactic:
have hcond := hcon Id (Xc ∩ Xd) (inter_subset_left.trans hXc.1) hId₁.of_delete hId₂.of_delete
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
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