internlm/Lean-Github huggingface dataset:
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 α
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
Proof state after:
no goals
Theorem: Matroid.exists_common_ind
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I, X, -, hI₁, hI₂, hcard⟩ := exists_common_ind_aux M₁ (M₂ ↾ M₁.E) rfl
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Theorem: Matroid.exists_common_ind
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ ∃ I X, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine ⟨I, (M₂.E \ M₁.E) ∪ X, hI₁, hI₂.of_restrict, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ I.ncard = M₁.r (M₂.E \ M₁.E ∪ X) + M₂.r (M₂.E \ (M₂.E \ M₁.E ∪ X))
Theorem: Matroid.exists_common_ind
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ I.ncard = M₁.r (M₂.E \ M₁.E ∪ X) + M₂.r (M₂.E \ (M₂.E \ M₁.E ∪ X))
Tactic:
rw [← diff_diff, diff_diff_right_self, r_eq_r_inter_ground, union_inter_distrib_right,
  disjoint_sdiff_left.inter_eq, empty_union, ← r_eq_r_inter_ground, hcard,
  restrict_r_eq _ (by simp [diff_subset]), restrict_ground_eq, M₂.r_eq_r_inter_ground,
  inter_diff_assoc, inter_comm]
Proof state after:
no goals
Theorem: Matroid.exists_common_ind
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I X : Set α
hI₁ : M₁.Indep I
hI₂ : (M₂ ↾ M₁.E).Indep I
hcard : I.ncard = M₁.r X + (M₂ ↾ M₁.E).r ((M₂ ↾ M₁.E).E \ X)
⊢ (M₂ ↾ M₁.E).E \ X ⊆ M₁.E
Tactic:
simp [diff_subset]
Proof state after:
no goals
Theorem: Matroid.exists_common_ind_with_flat_left
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₁.Flat X ∧ 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
this : M₂.Finite
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Theorem: Matroid.exists_common_ind_with_flat_left
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
this : M₂.Finite
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I,X, -, h1,h2, h⟩ := exists_common_ind_aux M₁ M₂ hE
Proof state after:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Theorem: Matroid.exists_common_ind_with_flat_left
Proof state before:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ∃ I X, M₁.Flat X ∧ M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine ⟨I, _, M₁.cl_flat X, h1, h2, (h1.ncard_le_r_add_r h2 _).antisymm ?_⟩
Proof state after:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r (M₁.cl X) + M₂.r (M₂.E \ M₁.cl X) ≤ I.ncard
Theorem: Matroid.exists_common_ind_with_flat_left
Proof state before:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r (M₁.cl X) + M₂.r (M₂.E \ M₁.cl X) ≤ I.ncard
Tactic:
rw [r_cl_eq, h, ← diff_inter_self_eq_diff (t := X), ← hE]
Proof state after:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r X + M₂.r (M₁.E \ M₁.cl X) ≤ M₁.r X + M₂.r (M₁.E \ (X ∩ M₁.E))
Theorem: Matroid.exists_common_ind_with_flat_left
Proof state before:
case 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
this : M₂.Finite
I X : Set α
h1 : M₁.Indep I
h2 : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ M₁.r X + M₂.r (M₁.E \ M₁.cl X) ≤ M₁.r X + M₂.r (M₁.E \ (X ∩ M₁.E))
Tactic:
exact add_le_add_left (M₂.r_mono (diff_subset_diff_right <| inter_ground_subset_cl M₁ X)) _
Proof state after:
no goals
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ I.ncard ≤ M₁.maxCommonInd M₂
Tactic:
rw [maxCommonInd, Nat.sSup_def, Nat.le_find_iff]
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ¬∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ m

case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∃ n, ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ n
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∃ n, ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ n
Tactic:
refine ⟨M₁.E.ncard, ?_⟩
Proof state after:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ M₁.E.ncard
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ M₁.E.ncard
Tactic:
simp only [mem_setOf_eq, forall_exists_index, and_imp]
Proof state after:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ (a : ℕ) (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ (a : ℕ) (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
Tactic:
rintro - J hJ₁ - rfl
Proof state after:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
J : Set α
hJ₁ : M₁.Indep J
⊢ J.ncard ≤ M₁.E.ncard
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
case h
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
J : Set α
hJ₁ : M₁.Indep J
⊢ J.ncard ≤ M₁.E.ncard
Tactic:
exact ncard_le_ncard hJ₁.subset_ground M₁.ground_finite
Proof state after:
no goals
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ¬∀ a ∈ {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}, a ≤ m
Tactic:
simp only [mem_setOf_eq, forall_exists_index, and_imp, not_forall, Classical.not_imp, not_le]
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ∃ x x_1, ∃ (_ : M₁.Indep x_1) (_ : M₂.Indep x_1) (_ : x_1.ncard = x), m < x
Theorem: Matroid.Indep.le_maxCommonInd
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
inst✝ : M₁.Finite
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
⊢ ∀ m < I.ncard, ∃ x x_1, ∃ (_ : M₁.Indep x_1) (_ : M₂.Indep x_1) (_ : x_1.ncard = x), m < x
Tactic:
exact fun m hm ↦ ⟨_, I, hI₁, hI₂, rfl, hm⟩
Proof state after:
no goals
Theorem: Matroid.maxCommonInd_exists
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = M₁.maxCommonInd M₂
Tactic:
refine Nat.sSup_mem (s := {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}) ⟨0, ∅, by simp⟩
  ⟨M₁.E.ncard, ?_⟩
Proof state after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.E.ncard ∈ upperBounds {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}
Theorem: Matroid.maxCommonInd_exists
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.E.ncard ∈ upperBounds {n | ∃ I, M₁.Indep I ∧ M₂.Indep I ∧ I.ncard = n}
Tactic:
simp only [upperBounds, mem_setOf_eq, forall_exists_index, and_imp]
Proof state after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∀ ⦃a : ℕ⦄ (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
Theorem: Matroid.maxCommonInd_exists
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ ∀ ⦃a : ℕ⦄ (x : Set α), M₁.Indep x → M₂.Indep x → x.ncard = a → a ≤ M₁.E.ncard
Tactic:
rintro _ I hI - rfl
Proof state after:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I : Set α
hI : M₁.Indep I
⊢ I.ncard ≤ M₁.E.ncard
Theorem: Matroid.maxCommonInd_exists
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
I : Set α
hI : M₁.Indep I
⊢ I.ncard ≤ M₁.E.ncard
Tactic:
exact ncard_le_ncard hI.subset_ground M₁.ground_finite
Proof state after:
no goals
Theorem: Matroid.maxCommonInd_exists
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝ : M₁.Finite
⊢ M₁.Indep ∅ ∧ M₂.Indep ∅ ∧ ∅.ncard = 0
Tactic:
simp
Proof state after:
no goals
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ M₁.maxCommonInd M₂ = ⨅ X, M₁.r X + M₂.r (M₂.E \ X)
Tactic:
refine le_antisymm (le_ciInf fun X ↦ ?_) ?_
Proof state after:
case refine_1
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X : Set α
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)

case refine_2
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
case refine_2
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Tactic:
obtain ⟨I, X, hI₁, hI₂, h⟩ := exists_common_ind M₁ M₂
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
case refine_2.intro.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ ⨅ X, M₁.r X + M₂.r (M₂.E \ X) ≤ M₁.maxCommonInd M₂
Tactic:
exact (ciInf_le ⟨0, by simp [lowerBounds]⟩ X).trans (h.symm.le.trans (hI₁.le_maxCommonInd hI₂))
Proof state after:
no goals
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
case refine_1
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X : Set α
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
obtain ⟨I, hI₁, hI₂, hI⟩ := maxCommonInd_exists M₁ M₂
Proof state after:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ M₁.maxCommonInd M₂ ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
rw [← hI]
Proof state after:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ I.ncard ≤ M₁.r X + M₂.r (M₂.E \ X)
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
case refine_1.intro.intro.intro
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
X I : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
hI : I.ncard = M₁.maxCommonInd M₂
⊢ I.ncard ≤ M₁.r X + M₂.r (M₂.E \ X)
Tactic:
exact hI₁.ncard_le_r_add_r hI₂ X
Proof state after:
no goals
Theorem: Matroid.matroid_intersection_minmax
Proof state before:
α : Type u_1
M M₁✝ M₂✝ : Matroid α
A I✝ X✝ E : Set α
M₁ M₂ : Matroid α
inst✝¹ : M₁.Finite
inst✝ : M₂.FiniteRk
I X : Set α
hI₁ : M₁.Indep I
hI₂ : M₂.Indep I
h : I.ncard = M₁.r X + M₂.r (M₂.E \ X)
⊢ 0 ∈ lowerBounds (range fun X => M₁.r X + M₂.r (M₂.E \ X))
Tactic:
simp [lowerBounds]
Proof state after:
no goals
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
have hinj : Function.Injective x := fun i j h ↦ by rw [← hx i, ← hx j, h]
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
have hS := (h_ind.subset (image_subset_range x S)).r
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = (x '' S).ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = (x '' S).ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
rw [ncard_image_of_injective _ hinj] at hS
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ S.ncard ≤ M.r (f ⁻¹' S)
Tactic:
refine hS.symm.le.trans (M.r_le_of_subset ?_)
Proof state after:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ x '' S ⊆ f ⁻¹' S
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
⊢ x '' S ⊆ f ⁻¹' S
Tactic:
rintro f ⟨i, hi, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
i : ι
hi : i ∈ S
⊢ x i ∈ f ⁻¹' S
Theorem: Matroid.rado_necessary
Proof state before:
case intro.intro
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
hinj : Function.Injective x
hS : M.r (x '' S) = S.ncard
i : ι
hi : i ∈ S
⊢ x i ∈ f ⁻¹' S
Tactic:
simpa [hx i]
Proof state after:
no goals
Theorem: Matroid.rado_necessary
Proof state before:
α : Type u_1
M M₁ M₂ : Matroid α
A I X E : Set α
ι : Type u_2
inst✝¹ : Finite ι
x : ι → α
inst✝ : M.FiniteRk
f : α → ι
hx : ∀ (i : ι), f (x i) = i
h_ind : M.Indep (range x)
S : Set ι
i j : ι
h : x i = x j
⊢ i = j
Tactic:
rw [← hx i, ← hx j, h]
Proof state after:
no goals
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof state before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ ¬LinearIndependent (ι := ↑↑s) R ((↑s).restrict f) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, c i ≠ 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
simp only [Finset.coe_sort_coe, not_linearIndependent_iff, Finset.univ_eq_attach, restrict_apply,
  ne_eq, Subtype.exists, Finset.mem_coe]
Proof state after:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ (∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof state before:
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
⊢ (∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0) ↔
    ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
Tactic:
refine ⟨fun ⟨g, hg0, b, hbs, hgb⟩ ↦ ?_, fun ⟨c,hc0,⟨b,hbs, hb0⟩,hc'⟩ ↦ ?_⟩
Proof state after:
case refine_1
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
g : { x // x ∈ s } → R
hg0 : ∑ x ∈ s.attach, g x • f ↑x = 0
b : ι
hbs : b ∈ s
hgb : ¬g ⟨b, hbs⟩ = 0
⊢ ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0

case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∃ g, ∑ x ∈ s.attach, g x • f ↑x = 0 ∧ ∃ a, ∃ (b : a ∈ s), ¬g ⟨a, b⟩ = 0
Tactic:
refine ⟨c ∘ Subtype.val, ?_, b, hbs, by simpa⟩
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, (c ∘ Subtype.val) x • f ↑x = 0
Theorem: Fintype.not_linearIndependent_restrict_iff
Proof state before:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, (c ∘ Subtype.val) x • f ↑x = 0
Tactic:
simp only [comp_apply]
Proof state after:
case refine_2
α : Type u_1
ι : Type u_2
W : Type u_3
W' : Type u_4
M : Type u_5
R : Type u_6
inst✝⁵ : AddCommGroup W
inst✝⁴ : AddCommGroup W'
inst✝³ : Fintype ι
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset ι
f : ι → M
x✝ : ∃ c, ∑ i : ι, c i • f i = 0 ∧ (∃ i ∈ s, ¬c i = 0) ∧ ∀ i ∉ s, c i = 0
c : ι → R
hc0 : ∑ i : ι, c i • f i = 0
b : ι
hbs : b ∈ s
hb0 : ¬c b = 0
hc' : ∀ i ∉ s, c i = 0
⊢ ∑ x ∈ s.attach, c ↑x • f ↑x = 0